1 /-
2 Copyright (c) 2018 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Mario Carneiro, Floris van Doorn
5
6 The (classical) real numbers ℝ. This is a direct construction
7 from Cauchy sequences.
8 -/
9 import order.conditionally_complete_lattice data.real.cau_seq_completion
src └──────────────────────────────────┘ └──────────────────────────┘
10 algebra.archimedean order.bounds
src └─────────────────┘ └──────────┘
11
12 def real := @cau_seq.completion.Cauchy ℚ _ _ _ abs _
id └───────────────────────┘ ┴ └─┘
src └───────────────────────┘ ┴ └─┘
typ └───────────────────────┘ ┴ └─┘
doc ┴
13 notation `ℝ` := real
id └──┘
src └──┘
typ └──┘
14
15 namespace real
16 open cau_seq cau_seq.completion
17
18 variables {x y : ℝ}
id ┴
src ┴
typ ┴
19
20 def of_rat (x : ℚ) : ℝ := of_rat x
id ┴ ┴ └────┘ ┴
src ┴ ┴ └────┘
typ ┴ ┴ └────┘ ┴
doc ┴
21
22 def mk (x : cau_seq ℚ abs) : ℝ := cau_seq.completion.mk x
id └─────┘ ┴ └─┘ ┴ └───────────────────┘ ┴
src └─────┘ ┴ └─┘ ┴ └───────────────────┘
typ └─────┘ ┴ └─┘ ┴ └───────────────────┘ ┴
doc ┴
23
24 def comm_ring_aux : comm_ring ℝ := cau_seq.completion.comm_ring
id └───────┘ ┴ └──────────────────────────┘
src └───────┘ ┴ └──────────────────────────┘
typ └───────┘ ┴ └──────────────────────────┘
25
26 instance : comm_ring ℝ := { ..comm_ring_aux }
id └───────┘ ┴ └───────────┘
src └───────┘ ┴ └───────────┘
typ └───────┘ ┴ └───────────┘
27
28 /- Extra instances to short-circuit type class resolution -/
29 instance : ring ℝ := by apply_instance
id └──┘ ┴
src └──┘ ┴ └─────────────┘
typ └──┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
30 instance : comm_semiring ℝ := by apply_instance
id └───────────┘ ┴
src └───────────┘ ┴ └─────────────┘
typ └───────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
31 instance : semiring ℝ := by apply_instance
id └──────┘ ┴
src └──────┘ ┴ └─────────────┘
typ └──────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
32 instance : add_comm_group ℝ := by apply_instance
id └────────────┘ ┴
src └────────────┘ ┴ └─────────────┘
typ └────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
33 instance : add_group ℝ := by apply_instance
id └───────┘ ┴
src └───────┘ ┴ └─────────────┘
typ └───────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
34 instance : add_comm_monoid ℝ := by apply_instance
id └─────────────┘ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
35 instance : add_monoid ℝ := by apply_instance
id └────────┘ ┴
src └────────┘ ┴ └─────────────┘
typ └────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
36 instance : add_left_cancel_semigroup ℝ := by apply_instance
id └───────────────────────┘ ┴
src └───────────────────────┘ ┴ └─────────────┘
typ └───────────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
37 instance : add_right_cancel_semigroup ℝ := by apply_instance
id └────────────────────────┘ ┴
src └────────────────────────┘ ┴ └─────────────┘
typ └────────────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
38 instance : add_comm_semigroup ℝ := by apply_instance
id └────────────────┘ ┴
src └────────────────┘ ┴ └─────────────┘
typ └────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
39 instance : add_semigroup ℝ := by apply_instance
id └───────────┘ ┴
src └───────────┘ ┴ └─────────────┘
typ └───────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
40 instance : comm_monoid ℝ := by apply_instance
id └─────────┘ ┴
src └─────────┘ ┴ └─────────────┘
typ └─────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
41 instance : monoid ℝ := by apply_instance
id └────┘ ┴
src └────┘ ┴ └─────────────┘
typ └────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
42 instance : comm_semigroup ℝ := by apply_instance
id └────────────┘ ┴
src └────────────┘ ┴ └─────────────┘
typ └────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
43 instance : semigroup ℝ := by apply_instance
id └───────┘ ┴
src └───────┘ ┴ └─────────────┘
typ └───────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
44 instance : inhabited ℝ := ⟨0⟩
id └───────┘ ┴
src └───────┘ ┴
typ └───────┘ ┴
45
46 theorem of_rat_sub (x y : ℚ) : of_rat (x - y) = of_rat x - of_rat y :=
id ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
src ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
doc ┴
47 congr_arg mk (const_sub _ _)
id └───────┘ └┘ └───────┘
src └───────┘ └┘ └───────┘
typ └───────┘ └┘ └───────┘
48
49 instance : has_lt ℝ :=
id └────┘ ┴
src └────┘ ┴
typ └────┘ ┴
50 ⟨λ x y, quotient.lift_on₂ x y (<) $
id ┴ ┴ └───────────────┘ ┴ ┴ ┴
src └───────────────┘ ┴
typ ┴ ┴ └───────────────┘ ┴ ┴ ┴
51 λ f₁ g₁ f₂ g₂ hf hg, propext $
id └┘ └┘ └┘ └┘ └┘ └┘ └─────┘
src └─────┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └─────┘
52 ⟨λ h, lt_of_eq_of_lt (setoid.symm hf) (lt_of_lt_of_eq h hg),
id ┴ └────────────┘ └─────────┘ └┘ └────────────┘ ┴ └┘
src └────────────┘ └─────────┘ └────────────┘
typ ┴ └────────────┘ └─────────┘ └┘ └────────────┘ ┴ └┘
53 λ h, lt_of_eq_of_lt hf (lt_of_lt_of_eq h (setoid.symm hg))⟩⟩
id ┴ └────────────┘ └┘ └────────────┘ ┴ └─────────┘ └┘
src └────────────┘ └────────────┘ └─────────┘
typ ┴ └────────────┘ └┘ └────────────┘ ┴ └─────────┘ └┘
54
55 @[simp] theorem mk_lt {f g : cau_seq ℚ abs} : mk f < mk g ↔ f < g := iff.rfl
id └─────┘ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─────┘ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─────┘
typ └─────┘ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ ┴
56
57 theorem mk_eq {f g : cau_seq ℚ abs} : mk f = mk g ↔ f ≈ g := mk_eq
id └─────┘ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘
src └─────┘ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └───┘
typ └─────┘ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘
doc ┴
58
59 theorem quotient_mk_eq_mk (f : cau_seq ℚ abs) : ⟦f⟧ = mk f := rfl
id └─────┘ ┴ └─┘ ┴┴┴ ┴ └┘ ┴ └─┘
src └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ └─┘
typ └─────┘ ┴ └─┘ ┴┴┴ ┴ └┘ ┴ └─┘
doc ┴
60
61 theorem mk_eq_mk {f : cau_seq ℚ abs} : cau_seq.completion.mk f = mk f := rfl
id └─────┘ ┴ └─┘ └───────────────────┘ ┴ ┴ └┘ ┴ └─┘
src └─────┘ ┴ └─┘ └───────────────────┘ ┴ └┘ └─┘
typ └─────┘ ┴ └─┘ └───────────────────┘ ┴ ┴ └┘ ┴ └─┘
doc ┴
62
63 @[simp] theorem mk_pos {f : cau_seq ℚ abs} : 0 < mk f ↔ pos f :=
id └─────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘ ┴
src └─────┘ ┴ └─┘ ┴ └┘ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘ ┴
doc └──┘ ┴ └─┘
64 iff_of_eq (congr_arg pos (sub_zero f))
id └───────┘ └───────┘ └─┘ └──────┘ ┴
src └───────┘ └───────┘ └─┘ └──────┘
typ └───────┘ └───────┘ └─┘ └──────┘ ┴
doc └─┘
65
66 protected def le (x y : ℝ) : Prop := x < y ∨ x = y
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
67 instance : has_le ℝ := ⟨real.le⟩
id └────┘ ┴ └─────┘
src └────┘ ┴ └─────┘
typ └────┘ ┴ └─────┘
68
69 @[simp] theorem mk_le {f g : cau_seq ℚ abs} : mk f ≤ mk g ↔ f ≤ g :=
id └─────┘ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─┘ └┘ ┴ └┘ ┴ ┴
typ └─────┘ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
70 or_congr iff.rfl quotient.eq
id └──────┘ └─────┘ └─────────┘
src └──────┘ └─────┘ └─────────┘
typ └──────┘ └─────┘ └─────────┘
71
72 theorem add_lt_add_iff_left {a b : ℝ} (c : ℝ) : c + a < c + b ↔ a < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
73 quotient.induction_on₃ a b c (λ f g h,
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
74 iff_of_eq (congr_arg pos $ by rw add_sub_add_left_eq_sub))
id └───────┘ └───────┘ └─┘ └─────────────────────┘
src └───────┘ └───────┘ └─┘ └─┘└─────────────────────┘
typ └───────┘ └───────┘ └─┘ └─┘└─────────────────────┘
doc └─┘ └─┘
txt └─┘
par └─┘
pid ┴
st └─────────────────────────┘
75
76 instance : linear_order ℝ :=
id └──────────┘ ┴
src └──────────┘ ┴
typ └──────────┘ ┴
77 { le := (≤), lt := (<),
id ┴ ┴
src ┴ ┴
typ ┴ ┴
78 le_refl := λ a, or.inr rfl,
id ┴ └────┘ └─┘
src └────┘ └─┘
typ ┴ └────┘ └─┘
79 le_trans := λ a b c, quotient.induction_on₃ a b c $
id ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴
src └────────────────────┘
typ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴
80 λ f g h, by simpa [quotient_mk_eq_mk] using le_trans,
id ┴ ┴ ┴ └───────────────┘ └──────┘
src └─────┘└───────────────┘└──────┘└──────┘
typ ┴ ┴ ┴ └─────┘└───────────────┘└──────┘└──────┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └───────────────────────────────────────┘
81 lt_iff_le_not_le := λ a b, quotient.induction_on₂ a b $
id ┴ ┴ └────────────────────┘ ┴ ┴
src └────────────────────┘
typ ┴ ┴ └────────────────────┘ ┴ ┴
82 λ f g, by simpa [quotient_mk_eq_mk] using lt_iff_le_not_le,
id ┴ ┴ └───────────────┘ └──────────────┘
src └─────┘└───────────────┘└──────┘└──────────────┘
typ ┴ ┴ └─────┘└───────────────┘└──────┘└──────────────┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └───────────────────────────────────────────────┘
83 le_antisymm := λ a b, quotient.induction_on₂ a b $
id ┴ ┴ └────────────────────┘ ┴ ┴
src └────────────────────┘
typ ┴ ┴ └────────────────────┘ ┴ ┴
84 λ f g, by simpa [mk_eq, quotient_mk_eq_mk] using @cau_seq.le_antisymm _ _ f g,
id ┴ ┴ └───┘ └───────────────┘ └─────────────────┘ ┴ ┴
src └─────┘└───┘└┘└───────────────┘└──────┘ └─────────────────┘└───┘ ┴
typ ┴ ┴ └─────┘└───┘└┘└───────────────┘└──────┘ └─────────────────┘└───┘┴┴┴
doc └─────┘ └┘ └──────┘ └───┘ ┴
txt └─────┘ └┘ └──────┘ └───┘ ┴
par └─────┘ └┘ └──────┘ └───┘ ┴
pid ┴┴ └┘ ┴┴└────┘ └───┘ ┴
st └──────────────────────────────────────────────────────────────────┘
85 le_total := λ a b, quotient.induction_on₂ a b $
id ┴ ┴ └────────────────────┘ ┴ ┴
src └────────────────────┘
typ ┴ ┴ └────────────────────┘ ┴ ┴
86 λ f g, by simpa [quotient_mk_eq_mk] using le_total f g }
id ┴ ┴ └───────────────┘ └──────┘ ┴ ┴
src └─────┘└───────────────┘└──────┘└──────┘┴ ┴ ┴
typ ┴ ┴ └─────┘└───────────────┘└──────┘└──────┘┴┴┴┴┴
doc └─────┘ └──────┘ ┴ ┴ ┴
txt └─────┘ └──────┘ ┴ ┴ ┴
par └─────┘ └──────┘ ┴ ┴ ┴
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴
st └────────────────────────────────────────────┘
87
88 instance : partial_order ℝ := by apply_instance
id └───────────┘ ┴
src └───────────┘ ┴ └─────────────┘
typ └───────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
89 instance : preorder ℝ := by apply_instance
id └──────┘ ┴
src └──────┘ ┴ └──────────────
typ └──────┘ ┴ └──────────────
doc └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
90
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
91 theorem of_rat_lt {x y : ℚ} : of_rat x < of_rat y ↔ x < y := const_lt
id ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
src ┴ └────┘ ┴ └────┘ ┴ ┴ └──────┘
typ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
doc ┴
92
93 protected theorem zero_lt_one : (0 : ℝ) < 1 := of_rat_lt.2 zero_lt_one
id ┴ ┴ └───────┘┴ └─────────┘
src ┴ ┴ └───────┘┴ └─────────┘
typ ┴ ┴ └───────┘┴ └─────────┘
94
95 protected theorem mul_pos {a b : ℝ} : 0 < a → 0 < b → 0 < a * b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
96 quotient.induction_on₂ a b $ λ f g,
id └────────────────────┘ ┴ ┴ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴
97 show pos (f - 0) → pos (g - 0) → pos (f * g - 0),
id └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
98 by simpa using cau_seq.mul_pos
id └─────────────┘
src └──────────┘└─────────────┘└
typ └──────────┘└─────────────┘└
doc └──────────┘ └
txt └──────────┘ └
par └──────────┘ └
pid ┴└────┘ └
st └────────────────────────────
99
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
100 instance : linear_ordered_comm_ring ℝ :=
id └──────────────────────┘ ┴
src └──────────────────────┘ ┴
typ └──────────────────────┘ ┴
101 { add_le_add_left := λ a b h c,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
102 (le_iff_le_iff_lt_iff_lt.2 $ real.add_lt_add_iff_left c).2 h,
id └─────────────────────┘┴ └──────────────────────┘ ┴ ┴ ┴
src └─────────────────────┘┴ └──────────────────────┘ ┴
typ └─────────────────────┘┴ └──────────────────────┘ ┴ ┴ ┴
103 zero_ne_one := ne_of_lt real.zero_lt_one,
id └──────┘ └──────────────┘
src └──────┘ └──────────────┘
typ └──────┘ └──────────────┘
104 mul_nonneg := λ a b a0 b0,
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
105 match a0, b0 with
id └┘ └┘
typ └┘ └┘
106 | or.inl a0, or.inl b0 := le_of_lt (real.mul_pos a0 b0)
id └┘ └────┘ └┘ └──────┘ └──────────┘
src └────┘ └──────┘ └──────────┘
typ └┘ └────┘ └┘ └──────┘ └──────────┘
107 | or.inr a0, _ := by simp [a0.symm]
id └────┘
src └────┘ └────┘ └─
typ └────┘ └────┘└─────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────
108 | _, or.inr b0 := by simp [b0.symm]
id └────┘
src ───┘ └────┘ └────┘ └─
typ ───┘ └────┘ └────┘└─────┘└─
doc ───┘ └────┘ └─
txt ───┘ └────┘ └─
par ───┘ └────┘ └─
pid ───┘ ┴┴ ┴└
st ───┘ └───────────────
109 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
110 mul_pos := @real.mul_pos,
id └──────────┘
src └──────────┘
typ └──────────┘
111 zero_lt_one := real.zero_lt_one,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
112 add_lt_add_left := λ a b h c, (real.add_lt_add_iff_left c).2 h,
id ┴ ┴ ┴ ┴ └──────────────────────┘ ┴ ┴ ┴
src └──────────────────────┘ ┴
typ ┴ ┴ ┴ ┴ └──────────────────────┘ ┴ ┴ ┴
113 ..real.comm_ring, ..real.linear_order }
id └────────────┘ └───────────────┘
src └────────────┘ └───────────────┘
typ └────────────┘ └───────────────┘
114
115 /- Extra instances to short-circuit type class resolution -/
116 instance : linear_ordered_ring ℝ := by apply_instance
id └─────────────────┘ ┴
src └─────────────────┘ ┴ └─────────────┘
typ └─────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
117 instance : ordered_ring ℝ := by apply_instance
id └──────────┘ ┴
src └──────────┘ ┴ └─────────────┘
typ └──────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
118 instance : linear_ordered_semiring ℝ := by apply_instance
id └─────────────────────┘ ┴
src └─────────────────────┘ ┴ └─────────────┘
typ └─────────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
119 instance : ordered_semiring ℝ := by apply_instance
id └──────────────┘ ┴
src └──────────────┘ ┴ └─────────────┘
typ └──────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
120 instance : ordered_comm_group ℝ := by apply_instance
id └────────────────┘ ┴
src └────────────────┘ ┴ └─────────────┘
typ └────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
121 instance : ordered_cancel_comm_monoid ℝ := by apply_instance
id └────────────────────────┘ ┴
src └────────────────────────┘ ┴ └─────────────┘
typ └────────────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
122 instance : ordered_comm_monoid ℝ := by apply_instance
id └─────────────────┘ ┴
src └─────────────────┘ ┴ └─────────────┘
typ └─────────────────┘ ┴ └─────────────┘
doc └─────────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
123 instance : domain ℝ := by apply_instance
id └────┘ ┴
src └────┘ ┴ └──────────────
typ └────┘ ┴ └──────────────
doc └────┘ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
124
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
125 open_locale classical
126
127 noncomputable instance : discrete_linear_ordered_field ℝ :=
id └───────────────────────────┘ ┴
src └───────────────────────────┘ ┴
typ └───────────────────────────┘ ┴
128 { decidable_le := by apply_instance,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
129 ..real.linear_ordered_comm_ring,
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
130 ..real.domain,
id └─────────┘
src └─────────┘
typ └─────────┘
131 ..cau_seq.completion.discrete_field }
id └───────────────────────────────┘
src └───────────────────────────────┘
typ └───────────────────────────────┘
132
133 /- Extra instances to short-circuit type class resolution -/
134
135 noncomputable instance : linear_ordered_field ℝ := by apply_instance
id └──────────────────┘ ┴
src └──────────────────┘ ┴ └─────────────┘
typ └──────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
136 noncomputable instance : decidable_linear_ordered_comm_ring ℝ := by apply_instance
id └────────────────────────────────┘ ┴
src └────────────────────────────────┘ ┴ └─────────────┘
typ └────────────────────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
137 noncomputable instance : decidable_linear_ordered_semiring ℝ := by apply_instance
id └───────────────────────────────┘ ┴
src └───────────────────────────────┘ ┴ └─────────────┘
typ └───────────────────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
138 noncomputable instance : decidable_linear_ordered_comm_group ℝ := by apply_instance
id └─────────────────────────────────┘ ┴
src └─────────────────────────────────┘ ┴ └─────────────┘
typ └─────────────────────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
139 noncomputable instance discrete_field : discrete_field ℝ := by apply_instance
id └────────────┘ ┴
src └────────────┘ ┴ └─────────────┘
typ └────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
140 noncomputable instance : field ℝ := by apply_instance
id └───┘ ┴
src └───┘ ┴ └─────────────┘
typ └───┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
141 noncomputable instance : division_ring ℝ := by apply_instance
id └───────────┘ ┴
src └───────────┘ ┴ └─────────────┘
typ └───────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
142 noncomputable instance : integral_domain ℝ := by apply_instance
id └─────────────┘ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
143 noncomputable instance : nonzero_comm_ring ℝ := by apply_instance
id └───────────────┘ ┴
src └───────────────┘ ┴ └─────────────┘
typ └───────────────┘ ┴ └─────────────┘
doc └───────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
144 noncomputable instance : decidable_linear_order ℝ := by apply_instance
id └────────────────────┘ ┴
src └────────────────────┘ ┴ └─────────────┘
typ └────────────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
145 noncomputable instance : lattice.distrib_lattice ℝ := by apply_instance
id └─────────────────────┘ ┴
src └─────────────────────┘ ┴ └─────────────┘
typ └─────────────────────┘ ┴ └─────────────┘
doc └─────────────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
146 noncomputable instance : lattice.lattice ℝ := by apply_instance
id └─────────────┘ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └─────────────┘
doc └─────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
147 noncomputable instance : lattice.semilattice_inf ℝ := by apply_instance
id └─────────────────────┘ ┴
src └─────────────────────┘ ┴ └─────────────┘
typ └─────────────────────┘ ┴ └─────────────┘
doc └─────────────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
148 noncomputable instance : lattice.semilattice_sup ℝ := by apply_instance
id └─────────────────────┘ ┴
src └─────────────────────┘ ┴ └─────────────┘
typ └─────────────────────┘ ┴ └─────────────┘
doc └─────────────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
149 noncomputable instance : lattice.has_inf ℝ := by apply_instance
id └─────────────┘ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └─────────────┘
doc └─────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
150 noncomputable instance : lattice.has_sup ℝ := by apply_instance
id └─────────────┘ ┴
src └─────────────┘ ┴ └──────────────
typ └─────────────┘ ┴ └──────────────
doc └─────────────┘ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
151
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
152 lemma le_of_forall_epsilon_le {a b : real} (h : ∀ε, ε > 0 → a ≤ b + ε) : a ≤ b :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
153 le_of_forall_le_of_dense $ assume x hxb,
id └──────────────────────┘ ┴ └─┘
src └──────────────────────┘
typ └──────────────────────┘ ┴ └─┘
154 calc a ≤ b + (x - b) : h (x-b) $ sub_pos.2 hxb
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─────┘┴ └─┘
src ┴ ┴ ┴ └─────┘┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─────┘┴ └─┘
155 ... = x : by rw [add_comm]; simp
id ┴ └──────┘
src └──┘└──────┘┴ └────
typ ┴ └──┘└──────┘┴ └────
doc └──┘ ┴ └────
txt └──┘ ┴ └────
par └──┘ ┴ └────
pid └┘ ┴ └
st └───────────┘┴└──────
156
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
157 open rat
158
159 @[simp] theorem of_rat_eq_cast : ∀ x : ℚ, of_rat x = x :=
id ┴ └────┘ ┴ ┴ ┴
src ┴ └────┘ ┴
typ ┴ └────┘ ┴ ┴ ┴
doc └──┘ ┴
160 eq_cast of_rat rfl of_rat_add of_rat_mul
id └─────┘ └────┘ └─┘ └────────┘ └────────┘
src └─────┘ └────┘ └─┘ └────────┘ └────────┘
typ └─────┘ └────┘ └─┘ └────────┘ └────────┘
161
162 theorem le_mk_of_forall_le {f : cau_seq ℚ abs} :
id └─────┘ ┴ └─┘
src └─────┘ ┴ └─┘
typ └─────┘ ┴ └─┘
doc ┴
163 (∃ i, ∀ j ≥ i, x ≤ f j) → x ≤ mk f :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
164 quotient.induction_on x $ λ g h, le_of_not_lt $
id └───────────────────┘ ┴ ┴ ┴ └──────────┘
src └───────────────────┘ └──────────┘
typ └───────────────────┘ ┴ ┴ ┴ └──────────┘
165 λ ⟨K, K0, hK⟩,
id ┴ └┘ └┘
typ ┴ └┘ └┘
166 let ⟨i, H⟩ := exists_forall_ge_and h $
id └─┘ └──────────────────┘ ┴
src └──────────────────┘
typ └─┘ └──────────────────┘ ┴
167 exists_forall_ge_and hK (f.cauchy₃ $ half_pos K0) in
id └──────────────────┘ ┴└──────┘ └──────┘
src └──────────────────┘ └──────┘ └──────┘
typ └──────────────────┘ ┴└──────┘ └──────┘
168 begin
st └─────
169 apply not_lt_of_le (H _ (le_refl _)).1,
id └──────────┘ ┴ └─────┘
src └────┘└──────────┘┴ └─┘ └─────┘└────┘
typ └────┘└──────────┘┴ ┴└─┘ └─────┘└────┘
doc └────┘ ┴ └─┘ └────┘
txt └────┘ ┴ └─┘ └────┘
par └────┘ ┴ └─┘ └────┘
pid ┴ ┴ └─┘ └──┘└┘
st ───────────────────────────────────────┘└─
170 rw ← of_rat_eq_cast,
id └────────────┘
src └───┘└────────────┘
typ └───┘└────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────────────────┘└─
171 refine ⟨_, half_pos K0, i, λ j ij, _⟩,
id └──────┘ └┘ ┴
src └─────┘ └─┘└──────┘┴ └┘ └┘ └───────┘
typ └─────┘ └─┘└──────┘┴└┘└┘┴└┘ └───────┘
doc └─────┘ └─┘ ┴ └┘ └┘ └───────┘
txt └─────┘ └─┘ ┴ └┘ └┘ └───────┘
par └─────┘ └─┘ ┴ └┘ └┘ └───────┘
pid ┴ └─┘ ┴ └┘ └┘ └───────┘
st ──────────────────────────────────────┘└─
172 have := add_le_add (H _ ij).2.1
id └────────┘
src └──────┘└────────┘┴ └─┘ └─────
typ └──────┘└────────┘┴ └─┘ └─────
doc └──────┘ ┴ └─┘ └─────
txt └──────┘ ┴ └─┘ └─────
par └──────┘ ┴ └─┘ └─────
pid └───┘└─┘ ┴ └─┘ └─────
st ──────────────────────────────────
173 (le_of_lt (abs_lt.1 $ (H _ (le_refl _)).2.2 _ ij).1),
id └──────┘ └────┘ ┴ └─────┘ └┘
src ───┘ └──────┘┴ └────┘└─┘ ┴ └─┘ └─────┘└─────────┘ └──┘
typ ───┘ └──────┘┴ └────┘└─┘ ┴ ┴└─┘ └─────┘└─────────┘└┘└──┘
doc ───┘ ┴ └─┘ ┴ └─┘ └─────────┘ └──┘
txt ───┘ ┴ └─┘ ┴ └─┘ └─────────┘ └──┘
par ───┘ ┴ └─┘ ┴ └─┘ └─────────┘ └──┘
pid ───┘ ┴ └─┘ ┴ └─┘ └─────────┘ └──┘
st ───────────────────────────────────────────────────────┘└─
174 rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this
id └────────────┘ └──────────────┘ └───────┘ └────────────────┘
src └─────┘└────────────┘└┘└──────────────┘└┘└───────┘└┘└────────────────┘└────────┘
typ └─────┘└────────────┘└┘└──────────────┘└┘└───────┘└┘└────────────────┘└────────┘
doc └─────┘ └┘ └┘ └┘ └────────┘
txt └─────┘ └┘ └┘ └┘ └────────┘
par └─────┘ └┘ └┘ └┘ └────────┘
pid └──┘ └┘ └┘ └┘ ┴└──────┘┴
st ──────────────────────┘└────────────────┘└─────────┘└──────────────────┘┴└───────┘
175 end
st └─┘
176
177 theorem mk_le_of_forall_le {f : cau_seq ℚ abs} {x : ℝ} :
id └─────┘ ┴ └─┘ ┴
src └─────┘ ┴ └─┘ ┴
typ └─────┘ ┴ └─┘ ┴
doc ┴
178 (∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) → mk f ≤ x
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
179 | ⟨i, H⟩ := by rw [← neg_le_neg_iff, ← mk_eq_mk, mk_neg]; exact
id └────────────┘ └──────┘ └────┘
src └────┘└────────────┘└──┘└──────┘└┘└────┘┴ └─────
typ └────┘└────────────┘└──┘└──────┘└┘└────┘┴ └─────
doc └────┘ └──┘ └┘ ┴ └─────
txt └────┘ └──┘ └┘ ┴ └─────
par └────┘ └──┘ └┘ ┴ └─────
pid └──┘ └──┘ └┘ ┴ └
st └───────────────────┘└──────────┘└──────┘┴└───────
180 le_mk_of_forall_le ⟨i, λ j ij, by simp [H _ ij]⟩
id └────────────────┘ ┴ ┴ └┘
src ─┘└────────────────┘┴ └┘ └─────┘ ┴└────┘ └─┘ ┴└─
typ ─┘└────────────────┘┴ ┴└┘ └─────┘ ┴└────┘┴└─┘└┘┴└─
doc ─┘ ┴ └┘ └─────┘ ┴└────┘ └─┘ ┴└─
txt ─┘ ┴ └┘ └─────┘ ┴└────┘ └─┘ ┴└─
par ─┘ ┴ └┘ └─────┘ ┴└────┘ └─┘ ┴└─
pid ─┘ ┴ └┘ └─────┘ └─────┘ └─┘ └┘└
st ──────────────────────────────────┘└────────────┘└─
181
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
182 theorem mk_near_of_forall_near {f : cau_seq ℚ abs} {x : ℝ} {ε : ℝ}
id └─────┘ ┴ └─┘ ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴
doc ┴
183 (H : ∃ i, ∀ j ≥ i, abs ((f j : ℝ) - x) ≤ ε) : abs (mk f - x) ≤ ε :=
id ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴
typ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴
184 abs_sub_le_iff.2
id └────────────┘┴
src └────────────┘┴
typ └────────────┘┴
185 ⟨sub_le_iff_le_add'.2 $ mk_le_of_forall_le $
id └────────────────┘┴ └────────────────┘
src └────────────────┘┴ └────────────────┘
typ └────────────────┘┴ └────────────────┘
186 H.imp $ λ i h j ij, sub_le_iff_le_add'.1 (abs_sub_le_iff.1 $ h j ij).1,
id ┴└──┘ ┴ ┴ ┴ └┘ └────────────────┘┴ └────────────┘┴ ┴ ┴ └┘ ┴
src └──┘ └────────────────┘┴ └────────────┘┴ ┴
typ ┴└──┘ ┴ ┴ ┴ └┘ └────────────────┘┴ └────────────┘┴ ┴ ┴ └┘ ┴
187 sub_le.1 $ le_mk_of_forall_le $
id └────┘┴ └────────────────┘
src └────┘┴ └────────────────┘
typ └────┘┴ └────────────────┘
188 H.imp $ λ i h j ij, sub_le.1 (abs_sub_le_iff.1 $ h j ij).2⟩
id ┴└──┘ ┴ ┴ ┴ └┘ └────┘┴ └────────────┘┴ ┴ ┴ └┘ ┴
src └──┘ └────┘┴ └────────────┘┴ ┴
typ ┴└──┘ ┴ ┴ ┴ └┘ └────┘┴ └────────────┘┴ ┴ ┴ └┘ ┴
189
190 instance : archimedean ℝ :=
id └─────────┘ ┴
src └─────────┘ ┴
typ └─────────┘ ┴
191 archimedean_iff_rat_le.2 $ λ x, quotient.induction_on x $ λ f,
id └────────────────────┘┴ ┴ └───────────────────┘ ┴ ┴
src └────────────────────┘┴ └───────────────────┘
typ └────────────────────┘┴ ┴ └───────────────────┘ ┴ ┴
192 let ⟨M, M0, H⟩ := f.bounded' 0 in
id └─┘ ┴ ┴ ┴└───────┘
src └───────┘
typ └─┘ ┴ ┴ ┴└───────┘
193 ⟨M, mk_le_of_forall_le ⟨0, λ i _,
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
194 rat.cast_le.2 $ le_of_lt (abs_lt.1 (H i)).2⟩⟩
id └─────────┘┴ └──────┘ └────┘┴ ┴ ┴
src └─────────┘┴ └──────┘ └────┘┴ ┴
typ └─────────┘┴ └──────┘ └────┘┴ ┴ ┴
195
196 /- mark `real` irreducible in order to prevent `auto_cases` unfolding reals,
197 since users rarely want to consider real numbers as Cauchy sequences.
198 Marking `comm_ring_aux` `irreducible` is done to ensure that there are no problems
199 with non definitionally equal instances, caused by making `real` irreducible-/
200 attribute [irreducible] real comm_ring_aux
id └──┘ └───────────┘
src └──┘ └───────────┘
typ └──┘ └───────────┘
doc └─────────┘
201
202 noncomputable instance : floor_ring ℝ := archimedean.floor_ring _
id └────────┘ ┴ └────────────────────┘
src └────────┘ ┴ └────────────────────┘
typ └────────┘ ┴ └────────────────────┘
doc └────────┘
203
204 theorem is_cau_seq_iff_lift {f : ℕ → ℚ} : is_cau_seq abs f ↔ is_cau_seq abs (λ i, (f i : ℝ)) :=
id ┴ ┴ └────────┘ └─┘ ┴ ┴ └────────┘ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ └────────┘ └─┘ ┴ └────────┘ └─┘ ┴
typ ┴ ┴ └────────┘ └─┘ ┴ ┴ └────────┘ └─┘ ┴ ┴ ┴ ┴
doc ┴ └────────┘ └────────┘
205 ⟨λ H ε ε0,
id ┴ ┴ └┘
typ ┴ ┴ └┘
206 let ⟨δ, δ0, δε⟩ := exists_pos_rat_lt ε0 in
id └─┘ └┘ └┘ └───────────────┘ └┘
src └───────────────┘
typ └─┘ └┘ └┘ └───────────────┘ └┘
207 (H _ δ0).imp $ λ i hi j ij, lt_trans
id ┴ └─┘ ┴ └┘ ┴ └┘ └──────┘
src └─┘ └──────┘
typ ┴ └─┘ ┴ └┘ ┴ └┘ └──────┘
208 (by simpa using (@rat.cast_lt ℝ _ _ _).2 (hi _ ij)) δε,
id └─────────┘ └┘ └┘
src └──────────┘ └─────────┘┴ └────────┘ └─┘ ┴
typ └──────────┘ └─────────┘┴ └────────┘ └┘└─┘└┘┴
doc └──────────┘ ┴ └────────┘ └─┘ ┴
txt └──────────┘ ┴ └────────┘ └─┘ ┴
par └──────────┘ ┴ └────────┘ └─┘ ┴
pid ┴└────┘ ┴ └────────┘ └─┘ ┴
st └─────────────────────────────────────────────┘
209 λ H ε ε0, (H _ (rat.cast_pos.2 ε0)).imp $
id ┴ ┴ └┘ ┴ └──────────┘┴ └┘ └─┘
src └──────────┘┴ └─┘
typ ┴ ┴ └┘ ┴ └──────────┘┴ └┘ └─┘
210 λ i hi j ij, (@rat.cast_lt ℝ _ _ _).1 $ by simpa using hi _ ij⟩
id ┴ └┘ ┴ └┘ └─────────┘ ┴ ┴ └┘ └┘
src └─────────┘ ┴ ┴ └──────────┘ └─┘
typ ┴ └┘ ┴ └┘ └─────────┘ ┴ ┴ └──────────┘└┘└─┘└┘
doc └──────────┘ └─┘
txt └──────────┘ └─┘
par └──────────┘ └─┘
pid ┴└────┘ └─┘
st └──────────────────┘
211
212 theorem of_near (f : ℕ → ℚ) (x : ℝ)
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
doc ┴
213 (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abs ((f j : ℝ) - x) < ε) :
id ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
214 ∃ h', real.mk ⟨f, h'⟩ = x :=
id ┴ └┘┴ └─────┘ ┴ └┘ ┴ ┴
src ┴ ┴ └─────┘ ┴
typ ┴ └┘┴ └─────┘ ┴ └┘ ┴ ┴
215 ⟨is_cau_seq_iff_lift.2 (of_near _ (const abs x) h),
id └─────────────────┘┴ └─────┘ └───┘ └─┘ ┴ ┴
src └─────────────────┘┴ └─────┘ └───┘ └─┘
typ └─────────────────┘┴ └─────┘ └───┘ └─┘ ┴ ┴
doc └───┘
216 sub_eq_zero.1 $ abs_eq_zero.1 $
id └─────────┘┴ └─────────┘┴
src └─────────┘┴ └─────────┘┴
typ └─────────┘┴ └─────────┘┴
217 eq_of_le_of_forall_le_of_dense (abs_nonneg _) $ λ ε ε0,
id └────────────────────────────┘ └────────┘ ┴ └┘
src └────────────────────────────┘ └────────┘
typ └────────────────────────────┘ └────────┘ ┴ └┘
218 mk_near_of_forall_near $
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
219 (h _ ε0).imp (λ i h j ij, le_of_lt (h j ij))⟩
id ┴ └┘ └─┘ ┴ ┴ ┴ └┘ └──────┘ ┴ ┴ └┘
src └─┘ └──────┘
typ ┴ └┘ └─┘ ┴ ┴ ┴ └┘ └──────┘ ┴ ┴ └┘
220
221 theorem exists_floor (x : ℝ) : ∃ (ub : ℤ), (ub:ℝ) ≤ x ∧
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
222 ∀ (z : ℤ), (z:ℝ) ≤ x → z ≤ ub :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
223 int.exists_greatest_of_bdd
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
224 (let ⟨n, hn⟩ := exists_int_gt x in ⟨n, λ z h',
id └─┘ ┴ └┘ └───────────┘ ┴ ┴ └┘
src └───────────┘
typ └─┘ ┴ └┘ └───────────┘ ┴ ┴ └┘
225 int.cast_le.1 $ le_trans h' $ le_of_lt hn⟩)
id └─────────┘┴ └──────┘ └┘ └──────┘
src └─────────┘┴ └──────┘ └──────┘
typ └─────────┘┴ └──────┘ └┘ └──────┘
226 (let ⟨n, hn⟩ := exists_int_lt x in ⟨n, le_of_lt hn⟩)
id └─┘ ┴ └┘ └───────────┘ ┴ └──────┘
src └───────────┘ └──────┘
typ └─┘ ┴ └┘ └───────────┘ ┴ └──────┘
227
228 theorem exists_sup (S : set ℝ) : (∃ x, x ∈ S) → (∃ x, ∀ y ∈ S, y ≤ x) →
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
229 ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
230 | ⟨L, hL⟩ ⟨U, hU⟩ := begin
st └─────
231 choose f hf using begin
src └────────────────┘ └
typ └────────────────┘ └
doc └────────────────┘ └
txt └────────────────┘ └
par └────────────────┘ └
pid └┘└─┘└─────┘ └
st ───────────────────┘└─────
232 refine λ d : ℕ, @int.exists_greatest_of_bdd
id └────────────────────────┘
src ───┘└─────┘ └───┘ └┘ └────────────────────────┘└
typ ───┘└─────┘ └───┘ └┘ └────────────────────────┘└
doc ───┘└─────┘ └───┘ └┘ └
txt ───┘└─────┘ └───┘ └┘ └
par ───┘└─────┘ └───┘ └┘ └
pid ──────────┘ └───┘ └┘ └
st ────────────────────────────────────────────────
233 (λ n, ∃ y ∈ S, (n:ℝ) ≤ y * d) _ _ _,
id ┴ ┴┴ ┴ ┴
src ─────┘ └──┘┴└───┘ ┴┴ ┴ └┘┴┴ ┴┴┴ └─────┘└─
typ ─────┘ └──┘┴└───┘┴┴┴ ┴ └┘┴┴ ┴┴┴ └─────┘└─
doc ─────┘ └──┘ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘└─
txt ─────┘ └──┘ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘└─
par ─────┘ └──┘ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘└─
pid ─────┘ └──┘ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └────────
st ────────────────────────────────────────┘└─
234 { cases exists_int_gt U with k hk,
id └───────────┘ ┴
src ─────┘└────┘└───────────┘┴ └────────┘└─
typ ─────┘└────┘└───────────┘┴┴└────────┘└─
doc ─────┘└────┘ ┴ └────────┘└─
txt ─────┘└────┘ ┴ └────────┘└─
par ─────┘└────┘ ┴ └────────┘└─
pid ───────────┘ ┴ └───────────
st ────┘└──────────────────────────────┘└─
235 refine ⟨k * d, λ z h, _⟩,
id ┴ ┴
src ─────┘└─────┘ ┴ ┴ └┘ └──────┘└─
typ ─────┘└─────┘ ┴┴ ┴┴└┘ └──────┘└─
doc ─────┘└─────┘ ┴ ┴ └┘ └──────┘└─
txt ─────┘└─────┘ ┴ ┴ └┘ └──────┘└─
par ─────┘└─────┘ ┴ ┴ └┘ └──────┘└─
pid ────────────┘ ┴ ┴ └┘ └─────────
st ─────────────────────────────┘└─
236 rcases h with ⟨y, yS, hy⟩,
id ┴
src ─────┘└─────┘ └───────────────┘└─
typ ─────┘└─────┘┴└───────────────┘└─
doc ─────┘└─────┘ └───────────────┘└─
txt ─────┘└─────┘ └───────────────┘└─
par ─────┘└─────┘ └───────────────┘└─
pid ────────────┘ └──────────────────
st ──────────────────────────────┘└─
237 refine int.cast_le.1 (le_trans hy _),
id └─────────┘ └──────┘ └┘
src ─────┘└─────┘└─────────┘└─┘ └──────┘┴ └─┘└─
typ ─────┘└─────┘└─────────┘└─┘ └──────┘┴└┘└─┘└─
doc ─────┘└─────┘ └─┘ ┴ └─┘└─
txt ─────┘└─────┘ └─┘ ┴ └─┘└─
par ─────┘└─────┘ └─┘ ┴ └─┘└─
pid ────────────┘ └─┘ ┴ └────
st ─────────────────────────────────────────┘└─
238 simp,
src ─────┘└──┘└─
typ ─────┘└──┘└─
doc ─────┘└──┘└─
txt ─────┘└──┘└─
par ─────┘└──┘└─
pid ────────────
st ─────────┘└─
239 exact mul_le_mul_of_nonneg_right
id └────────────────────────┘
src ─────┘└────┘└────────────────────────┘└
typ ─────┘└────┘└────────────────────────┘└
doc ─────┘└────┘ └
txt ─────┘└────┘ └
par ─────┘└────┘ └
pid ───────────┘ └
st ───────────────────────────────────────
240 (le_trans (hU _ yS) (le_of_lt hk)) (nat.cast_nonneg _) },
id └──────┘ └┘ └┘ └──────┘ └┘ └─────────────┘
src ───────┘ └──────┘┴ └─┘ └┘ └──────┘┴ └─┘ └─────────────┘└──┘└──
typ ───────┘ └──────┘┴ └┘└─┘└┘└┘ └──────┘┴└┘└─┘ └─────────────┘└──┘└──
doc ───────┘ ┴ └─┘ └┘ ┴ └─┘ └──┘└──
txt ───────┘ ┴ └─┘ └┘ ┴ └─┘ └──┘└──
par ───────┘ ┴ └─┘ └┘ ┴ └─┘ └──┘└──
pid ───────┘ ┴ └─┘ └┘ ┴ └─┘ └──────
st ──────────────────────────────────────────────────────────────┘┴└─
241 { exact ⟨⌊L * d⌋, L, hL, floor_le _⟩ }
id ┴ ┴┴ ┴ └┘ └──────┘
src ─────┘└────┘ ┴ ┴ ┴ ┴└┘ └┘ └┘└──────┘└──┘└─
typ ─────┘└────┘ ┴ ┴ ┴┴┴└┘┴└┘└┘└┘└──────┘└──┘└─
doc ─────┘└────┘ ┴ ┴ ┴ ┴└┘ └┘ └┘ └──┘└─
txt ─────┘└────┘ ┴ ┴ └┘ └┘ └┘ └──┘└─
par ─────┘└────┘ ┴ ┴ └┘ └┘ └┘ └──┘└─
pid ───────────┘ ┴ ┴ └┘ └┘ └┘ └─────
st ────────────────────────────────────────┘└─
242 end,
src ────┘
typ ────┘
doc ────┘
txt ────┘
par ────┘
pid ────┘
st ────┘└─
243 have hf₁ : ∀ n > 0, ∃ y ∈ S, ((f n / n:ℚ):ℝ) ≤ y := λ n n0,
id ┴ ┴┴ ┴ ┴
src └─────────┘ └────┘ ┴┴└───┘ ┴┴ ┴ ┴┴┴ ┴ └┘ └┘ ┴ └──┘ └──────
typ └─────────┘ └────┘ ┴┴└───┘┴┴┴ ┴┴ ┴┴┴ ┴ └┘ └┘ ┴ └──┘ └──────
doc └─────────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └──┘ └──────
txt └─────────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └──┘ └──────
par └─────────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └──┘ └──────
pid └──────┘└─┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └──┘ └──────
st ──────────────────────────────────────────────────────────────
244 let ⟨y, yS, hy⟩ := (hf n).1 in
id ┴ └┘ └┘
src ───┘ ┴ └┘ └┘ └───┘ ┴ └──────
typ ───┘ ┴ ┴└┘└┘└┘ └───┘ └┘┴ └──────
doc ───┘ ┴ └┘ └┘ └───┘ ┴ └──────
txt ───┘ ┴ └┘ └┘ └───┘ ┴ └──────
par ───┘ ┴ └┘ └┘ └───┘ ┴ └──────
pid ───┘ ┴ └┘ └┘ └───┘ ┴ └──────
st ───────────────────────────────────
245 ⟨y, yS, by simpa using (div_le_iff ((nat.cast_pos.2 n0):((_:ℝ) < _))).2 hy⟩,
id └────────┘ └──────────┘ └┘ ┴ └┘
src ───┘ └┘ └┘ ┴└──────────┘ └────────┘┴ └──────────┘└─┘ └┘ └┘ └┘┴└──────┘ ┴
typ ───┘ └┘ └┘ ┴└──────────┘ └────────┘┴ └──────────┘└─┘└┘└┘ └┘ └┘┴└──────┘└┘┴
doc ───┘ └┘ └┘ ┴└──────────┘ ┴ └─┘ └┘ └┘ └┘ └──────┘ ┴
txt ───┘ └┘ └┘ ┴└──────────┘ ┴ └─┘ └┘ └┘ └┘ └──────┘ ┴
par ───┘ └┘ └┘ ┴└──────────┘ ┴ └─┘ └┘ └┘ └┘ └──────┘ ┴
pid ───┘ └┘ └┘ └───────────┘ ┴ └─┘ └┘ └┘ └┘ └──────┘ ┴
st ─────────────┘└──────────────────────────────────────────────────────────────┘┴└─
246 have hf₂ : ∀ (n > 0) (y ∈ S), (y - (n:ℕ)⁻¹ : ℝ) < (f n / n:ℚ),
id ┴ ┴ ┴ └┘ ┴
src └─────────┘ └────────────┘ ┴ ┴ ┴┴┴ ┴ ┴└┘└─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────┘ └────────────┘┴┴ ┴ ┴┴┴┴ ┴ ┴└┘└─┘ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └─────────┘ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────────┘ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └──────┘└─┘ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
247 { intros n n0 y yS,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───┘└──────────────┘└─
248 have := lt_of_lt_of_le (sub_one_lt_floor _)
id └────────────┘ └──────────────┘
src └──────┘└────────────┘┴ └──────────────┘└───
typ └──────┘└────────────┘┴ └──────────────┘└───
doc └──────┘ ┴ └───
txt └──────┘ ┴ └───
par └──────┘ ┴ └───
pid └───┘└─┘ ┴ └───
st ────────────────────────────────────────────────
249 (int.cast_le.2 $ (hf n).2 _ ⟨y, yS, floor_le _⟩),
id └─────────┘ └┘ ┴ ┴ └┘ └──────┘
src ─────┘ └─────────┘└─┘ ┴ ┴ └────┘ └┘ └┘└──────┘└──┘
typ ─────┘ └─────────┘└─┘ ┴ └┘┴┴└────┘ ┴└┘└┘└┘└──────┘└──┘
doc ─────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └──┘
txt ─────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └──┘
par ─────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └──┘
pid ─────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └──┘
st ─────────────────────────────────────────────────────┘└─
250 simp [-sub_eq_add_neg],
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid ┴└───────────────┘
st ─────────────────────────┘└─
251 rwa [lt_div_iff ((nat.cast_pos.2 n0):((_:ℝ) < _)), sub_mul, _root_.inv_mul_cancel],
id └────────┘ └──────────┘ └┘ └─────┘ └───────────────────┘
src └───┘└────────┘┴ └──────────┘└─┘ └┘ └┘ └┘ └────┘└─────┘└┘└───────────────────┘┴
typ └───┘└────────┘┴ └──────────┘└─┘└┘└┘ └┘ └┘ └────┘└─────┘└┘└───────────────────┘┴
doc └───┘ ┴ └─┘ └┘ └┘ └┘ └────┘ └┘ ┴
txt └───┘ ┴ └─┘ └┘ └┘ └┘ └────┘ └┘ ┴
par └───┘ ┴ └─┘ └┘ └┘ └┘ └────┘ └┘ ┴
pid └┘ ┴ └─┘ └┘ └┘ └┘ └────┘ └┘ ┴
st ────────────────────────────────────────────────────┘└───────┘└─────────────────────┘┴└─
252 exact ne_of_gt (nat.cast_pos.2 n0) },
id └──────┘ └──────────┘ └┘
src └────┘└──────┘┴ └──────────┘└─┘ └┘
typ └────┘└──────┘┴ └──────────┘└─┘└┘└┘
doc └────┘ ┴ └─┘ └┘
txt └────┘ ┴ └─┘ └┘
par └────┘ ┴ └─┘ └┘
pid ┴ ┴ └─┘ ┴┴
st ──────────────────────────────────────┘└┘└
253 suffices hg, let g : cau_seq ℚ abs := ⟨λ n, f n / n, hg⟩,
id └─────┘ └─┘ ┴ └┘
src └─────────┘ └──────┘└─────┘┴ ┴└─┘└──┘ └──┘ ┴ ┴ ┴ └┘ ┴
typ └─────────┘ └──────┘└─────┘┴ ┴└─┘└──┘ └──┘┴┴ ┴ ┴ └┘└┘┴
doc └─────────┘ └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └┘ ┴
txt └─────────┘ └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └┘ ┴
par └─────────┘ └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └┘ ┴
pid └─────────┘ └───┘└─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └┘ ┴
st ────────────┘└───────────────────────────────────────────┘└─
254 refine ⟨mk g, λ y, ⟨λ h x xS, le_trans _ h, λ h, _⟩⟩,
id └┘ ┴ └──────┘
src └─────┘ └┘┴ └┘ └──┘ └───────┘└──────┘└─┘ └┘ └─────┘
typ └─────┘ └┘┴┴└┘ └──┘ └───────┘└──────┘└─┘ └┘ └─────┘
doc └─────┘ ┴ └┘ └──┘ └───────┘ └─┘ └┘ └─────┘
txt └─────┘ ┴ └┘ └──┘ └───────┘ └─┘ └┘ └─────┘
par └─────┘ ┴ └┘ └──┘ └───────┘ └─┘ └┘ └─────┘
pid ┴ ┴ └┘ └──┘ └───────┘ └─┘ └┘ └─────┘
st ─────────────────────────────────────────────────────┘└─
255 { refine le_of_forall_ge_of_dense (λ z xz, _),
id └──────────────────────┘
src └─────┘└──────────────────────┘┴ └───────┘
typ └─────┘└──────────────────────┘┴ └───────┘
doc └─────┘ ┴ └───────┘
txt └─────┘ ┴ └───────┘
par └─────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ───┘└─────────────────────────────────────────┘└─
256 cases exists_nat_gt (x - z)⁻¹ with K hK,
id └───────────┘ ┴ ┴
src └────┘└───────────┘┴ ┴ ┴ ┴ └────────┘
typ └────┘└───────────┘┴ ┴┴ ┴┴┴ └────────┘
doc └────┘ ┴ ┴ ┴ ┴ └────────┘
txt └────┘ ┴ ┴ ┴ ┴ └────────┘
par └────┘ ┴ ┴ ┴ ┴ └────────┘
pid ┴ ┴ ┴ ┴ ┴ └────────┘
st ──────────────────────────────────────────┘└─
257 refine le_mk_of_forall_le ⟨K, λ n nK, _⟩,
id └────────────────┘ ┴
src └─────┘└────────────────┘┴ └┘ └───────┘
typ └─────┘└────────────────┘┴ ┴└┘ └───────┘
doc └─────┘ ┴ └┘ └───────┘
txt └─────┘ ┴ └┘ └───────┘
par └─────┘ ┴ └┘ └───────┘
pid ┴ ┴ └┘ └───────┘
st ───────────────────────────────────────────┘└─
258 replace xz := sub_pos.2 xz,
id └─────┘ └┘
src └────────────┘└─────┘└─┘
typ └────────────┘└─────┘└─┘└┘
doc └────────────┘ └─┘
txt └────────────┘ └─┘
par └────────────┘ └─┘
pid └─┘┴└─┘ └─┘
st ─────────────────────────────┘└─
259 replace hK := le_trans (le_of_lt hK) (nat.cast_le.2 nK),
id └──────┘ └──────┘ └┘ └─────────┘ └┘
src └────────────┘└──────┘┴ └──────┘┴ └┘ └─────────┘└─┘ ┴
typ └────────────┘└──────┘┴ └──────┘┴└┘└┘ └─────────┘└─┘└┘┴
doc └────────────┘ ┴ ┴ └┘ └─┘ ┴
txt └────────────┘ ┴ ┴ └┘ └─┘ ┴
par └────────────┘ ┴ ┴ └┘ └─┘ ┴
pid └─┘┴└─┘ ┴ ┴ └┘ └─┘ ┴
st ──────────────────────────────────────────────────────────┘└─
260 have n0 : 0 < n := nat.cast_pos.1 (lt_of_lt_of_le (inv_pos xz) hK),
id ┴ └──────────┘ └────────────┘ └─────┘ └┘ └┘
src └──────────┘ ┴ └──┘└──────────┘└─┘ └────────────┘┴ └─────┘┴ └┘ ┴
typ └──────────┘ ┴┴└──┘└──────────┘└─┘ └────────────┘┴ └─────┘┴└┘└┘└┘┴
doc └──────────┘ ┴ └──┘ └─┘ ┴ ┴ └┘ ┴
txt └──────────┘ ┴ └──┘ └─┘ ┴ ┴ └┘ ┴
par └──────────┘ ┴ └──┘ └─┘ ┴ ┴ └┘ ┴
pid └─────┘└───┘ ┴ └──┘ └─┘ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
261 refine le_trans _ (le_of_lt $ hf₂ _ n0 _ xS),
id └──────┘ └──────┘ └─┘ └┘ └┘
src └─────┘└──────┘└─┘ └──────┘┴ ┴ └─┘ └─┘ ┴
typ └─────┘└──────┘└─┘ └──────┘┴ ┴└─┘└─┘└┘└─┘└┘┴
doc └─────┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
txt └─────┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
par └─────┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
pid ┴ └─┘ ┴ ┴ └─┘ └─┘ ┴
st ───────────────────────────────────────────────┘└─
262 rwa [le_sub, inv_le ((nat.cast_pos.2 n0):((_:ℝ) < _)) xz] },
id └────┘ └────┘ └──────────┘ └┘ └┘
src └───┘└────┘└┘└────┘┴ └──────────┘└─┘ └┘ └┘ └┘ └───┘ └┘
typ └───┘└────┘└┘└────┘┴ └──────────┘└─┘└┘└┘ └┘ └┘ └───┘└┘└┘
doc └───┘ └┘ ┴ └─┘ └┘ └┘ └┘ └───┘ └┘
txt └───┘ └┘ ┴ └─┘ └┘ └┘ └┘ └───┘ └┘
par └───┘ └┘ ┴ └─┘ └┘ └┘ └┘ └───┘ └┘
pid └┘ └┘ ┴ └─┘ └┘ └┘ └┘ └───┘ ┴┴
st ──────────────┘└───────────────────────────────────────────┘┴┴└┘└
263 { exact mk_le_of_forall_le ⟨1, λ n n1,
id └────────────────┘
src └────┘└────────────────┘┴ └─┘ └──────
typ └────┘└────────────────┘┴ └─┘ └──────
doc └────┘ ┴ └─┘ └──────
txt └────┘ ┴ └─┘ └──────
par └────┘ ┴ └─┘ └──────
pid ┴ ┴ └─┘ └──────
st ───┘└────────────────────────────────────
264 let ⟨x, xS, hx⟩ := hf₁ _ n1 in le_trans hx (h _ xS)⟩ },
id └┘ └┘ └─┘ └──────┘ ┴
src ─────┘ ┴ └┘ └┘ └───┘ └─┘ └──┘└──────┘┴ ┴ └─┘ └─┘
typ ─────┘ ┴ └┘└┘└┘└┘└───┘└─┘└─┘ └──┘└──────┘┴ ┴ ┴└─┘ └─┘
doc ─────┘ ┴ └┘ └┘ └───┘ └─┘ └──┘ ┴ ┴ └─┘ └─┘
txt ─────┘ ┴ └┘ └┘ └───┘ └─┘ └──┘ ┴ ┴ └─┘ └─┘
par ─────┘ ┴ └┘ └┘ └───┘ └─┘ └──┘ ┴ ┴ └─┘ └─┘
pid ─────┘ ┴ └┘ └┘ └───┘ └─┘ └──┘ ┴ ┴ └─┘ └┘┴
st ──────────────────────────────────────────────────────────┘└┘└
265 intros ε ε0,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
266 suffices : ∀ j k ≥ nat_ceil ε⁻¹, (f j / j - f k / k : ℚ) < ε,
id └──────┘ ┴ ┴
src └─────────┘ └─────┘└──────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴
typ └─────────┘ └─────┘└──────┘┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ └─┘ └┘ ┴┴
doc └─────────┘ └─────┘└──────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴
txt └─────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴
par └─────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴
pid └───────┘└┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴
st ─────────────────────────────────────────────────────────────┘└─
267 { refine ⟨_, λ j ij, abs_lt.2 ⟨_, this _ _ ij (le_refl _)⟩⟩,
id └────┘ └──┘ └─────┘
src └─────┘ └─┘ └─────┘└────┘└─┘ └─┘ └───┘ ┴ └─────┘└───┘
typ └─────┘ └─┘ └─────┘└────┘└─┘ └─┘└──┘└───┘ ┴ └─────┘└───┘
doc └─────┘ └─┘ └─────┘ └─┘ └─┘ └───┘ ┴ └───┘
txt └─────┘ └─┘ └─────┘ └─┘ └─┘ └───┘ ┴ └───┘
par └─────┘ └─┘ └─────┘ └─┘ └─┘ └───┘ ┴ └───┘
pid ┴ └─┘ └─────┘ └─┘ └─┘ └───┘ ┴ └───┘
st ───┘└───────────────────────────────────────────────────────┘└─
268 rw [neg_lt, neg_sub], exact this _ _ (le_refl _) ij },
id └────┘ └─────┘ └──┘ └─────┘ └┘
src └──┘└────┘└┘└─────┘┴ └────┘ └───┘ └─────┘└──┘ ┴
typ └──┘└────┘└┘└─────┘┴ └────┘└──┘└───┘ └─────┘└──┘└┘┴
doc └──┘ └┘ ┴ └────┘ └───┘ └──┘ ┴
txt └──┘ └┘ ┴ └────┘ └───┘ └──┘ ┴
par └──┘ └┘ ┴ └────┘ └───┘ └──┘ ┴
pid └┘ └┘ ┴ ┴ └───┘ └──┘ ┴
st ─────────────┘└───────┘└───────────────────────────────┘└┘└
269 intros j k ij ik,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────┘└─
270 replace ij := le_trans (le_nat_ceil _) (nat.cast_le.2 ij),
id └──────┘ └─────────┘ └─────────┘ └┘
src └────────────┘└──────┘┴ └─────────┘└──┘ └─────────┘└─┘ ┴
typ └────────────┘└──────┘┴ └─────────┘└──┘ └─────────┘└─┘└┘┴
doc └────────────┘ ┴ └──┘ └─┘ ┴
txt └────────────┘ ┴ └──┘ └─┘ ┴
par └────────────┘ ┴ └──┘ └─┘ ┴
pid └─┘┴└─┘ ┴ └──┘ └─┘ ┴
st ──────────────────────────────────────────────────────────┘└─
271 replace ik := le_trans (le_nat_ceil _) (nat.cast_le.2 ik),
id └──────┘ └─────────┘ └─────────┘ └┘
src └────────────┘└──────┘┴ └─────────┘└──┘ └─────────┘└─┘ ┴
typ └────────────┘└──────┘┴ └─────────┘└──┘ └─────────┘└─┘└┘┴
doc └────────────┘ ┴ └──┘ └─┘ ┴
txt └────────────┘ ┴ └──┘ └─┘ ┴
par └────────────┘ ┴ └──┘ └─┘ ┴
pid └─┘┴└─┘ ┴ └──┘ └─┘ ┴
st ──────────────────────────────────────────────────────────┘└─
272 have j0 := nat.cast_pos.1 (lt_of_lt_of_le (inv_pos ε0) ij),
id └──────────┘ └────────────┘ └─────┘ └┘ └┘
src └─────────┘└──────────┘└─┘ └────────────┘┴ └─────┘┴ └┘ ┴
typ └─────────┘└──────────┘└─┘ └────────────┘┴ └─────┘┴└┘└┘└┘┴
doc └─────────┘ └─┘ ┴ ┴ └┘ ┴
txt └─────────┘ └─┘ ┴ ┴ └┘ ┴
par └─────────┘ └─┘ ┴ ┴ └┘ ┴
pid └─────┘┴└─┘ └─┘ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────┘└─
273 have k0 := nat.cast_pos.1 (lt_of_lt_of_le (inv_pos ε0) ik),
id └──────────┘ └────────────┘ └─────┘ └┘ └┘
src └─────────┘└──────────┘└─┘ └────────────┘┴ └─────┘┴ └┘ ┴
typ └─────────┘└──────────┘└─┘ └────────────┘┴ └─────┘┴└┘└┘└┘┴
doc └─────────┘ └─┘ ┴ ┴ └┘ ┴
txt └─────────┘ └─┘ ┴ ┴ └┘ ┴
par └─────────┘ └─┘ ┴ ┴ └┘ ┴
pid └─────┘┴└─┘ └─┘ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────┘└─
274 rcases hf₁ _ j0 with ⟨y, yS, hy⟩,
id └─┘ └┘
src └─────┘ └─┘ └───────────────┘
typ └─────┘└─┘└─┘└┘└───────────────┘
doc └─────┘ └─┘ └───────────────┘
txt └─────┘ └─┘ └───────────────┘
par └─────┘ └─┘ └───────────────┘
pid ┴ └─┘ └───────────────┘
st ─────────────────────────────────┘└─
275 refine lt_of_lt_of_le ((@rat.cast_lt ℝ _ _ _).1 _)
id └────────────┘ └─────────┘
src └─────┘└────────────┘┴ └─────────┘┴ └────────────
typ └─────┘└────────────┘┴ └─────────┘┴ └────────────
doc └─────┘ ┴ ┴ └────────────
txt └─────┘ ┴ ┴ └────────────
par └─────┘ ┴ ┴ └────────────
pid ┴ ┴ ┴ └────────────
st ─────────────────────────────────────────────────────
276 ((inv_le ε0 (nat.cast_pos.2 k0)).1 ik),
id └────┘ └┘ └──────────┘ └┘ └┘
src ───┘ └────┘┴ ┴ └──────────┘└─┘ └───┘ ┴
typ ───┘ └────┘┴└┘┴ └──────────┘└─┘└┘└───┘└┘┴
doc ───┘ ┴ ┴ └─┘ └───┘ ┴
txt ───┘ ┴ ┴ └─┘ └───┘ ┴
par ───┘ ┴ ┴ └─┘ └───┘ ┴
pid ───┘ ┴ ┴ └─┘ └───┘ ┴
st ─────────────────────────────────────────┘└─
277 simpa using sub_lt_iff_lt_add'.2
id └────────────────┘
src └──────────┘└────────────────┘└──
typ └──────────┘└────────────────┘└──
doc └──────────┘ └──
txt └──────────┘ └──
par └──────────┘ └──
pid ┴└────┘ └──
st ───────────────────────────────────
278 (lt_of_le_of_lt hy $ sub_lt_iff_lt_add.1 $ hf₂ _ k0 _ yS)
id └────────────┘ └┘ └───────────────┘ └─┘ └┘ └┘
src ───┘ └────────────┘┴ ┴ ┴└───────────────┘└─┘ ┴ └─┘ └─┘ └┘
typ ───┘ └────────────┘┴└┘┴ ┴└───────────────┘└─┘ ┴└─┘└─┘└┘└─┘└┘└┘
doc ───┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘ └┘
txt ───┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘ └┘
par ───┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘ └┘
pid ───┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘ ┴┴
st ─────────────────────────────────────────────────────────────┘
279 end
st └─┘
280
281 noncomputable def Sup (S : set ℝ) : ℝ :=
id └─┘ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴
282 if h : (∃ x, x ∈ S) ∧ (∃ x, ∀ y ∈ S, y ≤ x)
id └┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
283 then classical.some (exists_sup S h.1 h.2) else 0
id └────────────┘ └────────┘ ┴ ┴┴ ┴┴ ┴
src └────────────┘ └────────┘ ┴ ┴ ┴
typ └────────────┘ └────────┘ ┴ ┴┴ ┴┴ ┴
284
285 theorem Sup_le (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x)
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
286 {y} : Sup S ≤ y ↔ ∀ z ∈ S, z ≤ y :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
287 by simp [Sup, h₁, h₂]; exact
id └─┘ └┘ └┘
src └────┘└─┘└┘ └┘ ┴ └────┘
typ └────┘└─┘└┘└┘└┘└┘┴ └────┘
doc └────┘ └┘ └┘ ┴ └────┘
txt └────┘ └┘ └┘ ┴ └────┘
par └────┘ └┘ └┘ ┴ └────┘
pid ┴┴ └┘ └┘ ┴ ┴
st └──────────────────────────
288 classical.some_spec (exists_sup S h₁ h₂) y
id └─────────────────┘ └────────┘ ┴ └┘ └┘ ┴
src └─────────────────┘┴ └────────┘┴ ┴ ┴ └┘ └
typ └─────────────────┘┴ └────────┘┴┴┴└┘┴└┘└┘┴└
doc ┴ ┴ ┴ ┴ └┘ └
txt ┴ ┴ ┴ ┴ └┘ └
par ┴ ┴ ┴ ┴ └┘ └
pid ┴ ┴ ┴ ┴ └┘ └
st ───────────────────────────────────────────
289
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
290 section
291 -- this proof times out without this
292 local attribute [instance, priority 1000] classical.prop_decidable
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
293 theorem lt_Sup (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x)
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
294 {y} : y < Sup S ↔ ∃ z ∈ S, y < z :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
295 by simpa [not_forall] using not_congr (@Sup_le S h₁ h₂ y)
id └────────┘ └───────┘ └────┘ ┴ └┘ └┘ ┴
src └─────┘└────────┘└──────┘└───────┘┴ └────┘┴ ┴ ┴ ┴ └┘
typ └─────┘└────────┘└──────┘└───────┘┴ └────┘┴┴┴└┘┴└┘┴┴└┘
doc └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └┘
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴┴
st └──────────────────────────────────────────────────────┘
296 end
297
298 theorem le_Sup (S : set ℝ) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x) {x} (xS : x ∈ S) : x ≤ Sup S :=
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
299 (Sup_le S ⟨_, xS⟩ h₂).1 (le_refl _) _ xS
id └────┘ ┴ └┘ └┘ ┴ └─────┘ └┘
src └────┘ ┴ └─────┘
typ └────┘ ┴ └┘ └┘ ┴ └─────┘ └┘
300
301 theorem Sup_le_ub (S : set ℝ) (h₁ : ∃ x, x ∈ S) {ub} (h₂ : ∀ y ∈ S, y ≤ ub) : Sup S ≤ ub :=
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ └┘
src └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ └┘
302 (Sup_le S h₁ ⟨_, h₂⟩).2 h₂
id └────┘ ┴ └┘ └┘ ┴ └┘
src └────┘ ┴
typ └────┘ ┴ └┘ └┘ ┴ └┘
303
304 protected lemma is_lub_Sup {s : set ℝ} {a b : ℝ} (ha : a ∈ s) (hb : b ∈ upper_bounds s) :
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
src └─┘ ┴ ┴ ┴ ┴ └──────────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘
305 is_lub s (Sup s) :=
id └────┘ ┴ └─┘ ┴
src └────┘ └─┘
typ └────┘ ┴ └─┘ ┴
doc └────┘
306 ⟨λ x xs, real.le_Sup s ⟨_, hb⟩ xs,
id ┴ └┘ └─────────┘ ┴ └┘ └┘
src └─────────┘
typ ┴ └┘ └─────────┘ ┴ └┘ └┘
307 λ u h, real.Sup_le_ub _ ⟨_, ha⟩ h⟩
id ┴ ┴ └────────────┘ └┘ ┴
src └────────────┘
typ ┴ ┴ └────────────┘ └┘ ┴
308
309 noncomputable def Inf (S : set ℝ) : ℝ := -Sup {x | -x ∈ S}
id └─┘ ┴ ┴ ┴└─┘ ┴┴ ┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴└─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴└─┘ ┴┴ ┴┴ ┴ ┴
310
311 theorem le_Inf (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, x ≤ y)
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
312 {y} : y ≤ Inf S ↔ ∀ z ∈ S, y ≤ z :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
313 begin
st └─────
314 refine le_neg.trans ((Sup_le _ _ _).trans _),
id └──────────┘ └────┘
src └─────┘└──────────┘┴ └────┘└──────────────┘
typ └─────┘└──────────┘┴ └────┘└──────────────┘
doc └─────┘ ┴ └──────────────┘
txt └─────┘ ┴ └──────────────┘
par └─────┘ ┴ └──────────────┘
pid ┴ ┴ └──────────────┘
st ─────────────────────────────────────────────┘└─
315 { cases h₁ with x xS, exact ⟨-x, by simp [xS]⟩ },
id └┘ ┴┴ └┘
src └────┘ └────────┘ └────┘ ┴ └┘ ┴└────┘ ┴└┘
typ └────┘└┘└────────┘ └────┘ ┴┴└┘ ┴└────┘└┘┴└┘
doc └────┘ └────────┘ └────┘ └┘ ┴└────┘ ┴└┘
txt └────┘ └────────┘ └────┘ └┘ ┴└────┘ ┴└┘
par └────┘ └────────┘ └────┘ └┘ ┴└────┘ ┴└┘
pid ┴ └────────┘ ┴ └┘ └─────┘ └┘┴
st ───┘└────────────────┘└─────────────┘└────────┘└┘└┘└
316 { cases h₂ with ub h, exact ⟨-ub, λ y hy, le_neg.1 $ h _ hy⟩ },
id └┘ └┘ └────┘ ┴
src └────┘ └────────┘ └────┘ └┘ └─────┘└────┘└─┘ ┴ └─┘ └┘
typ └────┘└┘└────────┘ └────┘ └┘└┘ └─────┘└────┘└─┘ ┴┴└─┘ └┘
doc └────┘ └────────┘ └────┘ └┘ └─────┘ └─┘ ┴ └─┘ └┘
txt └────┘ └────────┘ └────┘ └┘ └─────┘ └─┘ ┴ └─┘ └┘
par └────┘ └────────┘ └────┘ └┘ └─────┘ └─┘ ┴ └─┘ └┘
pid ┴ └────────┘ ┴ └┘ └─────┘ └─┘ ┴ └─┘ ┴┴
st ───┘└────────────────┘└───────────────────────────────────────┘└┘└
317 split; intros H z hz,
src └───┘ └───────────┘
typ └───┘ └───────────┘
doc └───┘ └───────────┘
txt └───┘ └───────────┘
par └───┘ └───────────┘
pid └─────┘
st ─────────────────────┘└─
318 { exact neg_le_neg_iff.1 (H _ $ by simp [hz]) },
id └────────────┘ ┴ └┘
src └────┘└────────────┘└─┘ └─┘ ┴ ┴└────┘ ┴└┘
typ └────┘└────────────┘└─┘ ┴└─┘ ┴ ┴└────┘└┘┴└┘
doc └────┘ └─┘ └─┘ ┴ ┴└────┘ ┴└┘
txt └────┘ └─┘ └─┘ ┴ ┴└────┘ ┴└┘
par └────┘ └─┘ └─┘ ┴ ┴└────┘ ┴└┘
pid ┴ └─┘ └─┘ ┴ └─────┘ └┘┴
st ───┘└──────────────────────────────┘└────────┘└┘└┘└
319 { exact le_neg.2 (H _ hz) }
id └────┘ ┴ └┘
src └────┘└────┘└─┘ └─┘ └┘
typ └────┘└────┘└─┘ ┴└─┘└┘└┘
doc └────┘ └─┘ └─┘ └┘
txt └────┘ └─┘ └─┘ └┘
par └────┘ └─┘ └─┘ └┘
pid ┴ └─┘ └─┘ ┴┴
st ───────────────────────────┘└─
320 end
st ──┘
321
322 section
323 -- this proof times out without this
324 local attribute [instance, priority 1000] classical.prop_decidable
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
325 theorem Inf_lt (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, x ≤ y)
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
326 {y} : Inf S < y ↔ ∃ z ∈ S, z < y :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
327 by simpa [not_forall] using not_congr (@le_Inf S h₁ h₂ y)
id └────────┘ └───────┘ └────┘ ┴ └┘ └┘ ┴
src └─────┘└────────┘└──────┘└───────┘┴ └────┘┴ ┴ ┴ ┴ └┘
typ └─────┘└────────┘└──────┘└───────┘┴ └────┘┴┴┴└┘┴└┘┴┴└┘
doc └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └┘
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴┴
st └──────────────────────────────────────────────────────┘
328 end
329
330 theorem Inf_le (S : set ℝ) (h₂ : ∃ x, ∀ y ∈ S, x ≤ y) {x} (xS : x ∈ S) : Inf S ≤ x :=
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
331 (le_Inf S ⟨_, xS⟩ h₂).1 (le_refl _) _ xS
id └────┘ ┴ └┘ └┘ ┴ └─────┘ └┘
src └────┘ ┴ └─────┘
typ └────┘ ┴ └┘ └┘ ┴ └─────┘ └┘
332
333 theorem lb_le_Inf (S : set ℝ) (h₁ : ∃ x, x ∈ S) {lb} (h₂ : ∀ y ∈ S, lb ≤ y) : lb ≤ Inf S :=
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
334 (le_Inf S h₁ ⟨_, h₂⟩).2 h₂
id └────┘ ┴ └┘ └┘ ┴ └┘
src └────┘ ┴
typ └────┘ ┴ └┘ └┘ ┴ └┘
335
336 open lattice
337 noncomputable instance lattice : lattice ℝ := by apply_instance
id └─────┘ ┴
src └─────┘ ┴ └──────────────
typ └─────┘ ┴ └──────────────
doc └─────┘ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
338
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
339 noncomputable instance : conditionally_complete_linear_order ℝ :=
id └─────────────────────────────────┘ ┴
src └─────────────────────────────────┘ ┴
typ └─────────────────────────────────┘ ┴
340 { Sup := real.Sup,
id └──────┘
src └──────┘
typ └──────┘
341 Inf := real.Inf,
id └──────┘
src └──────┘
typ └──────┘
342 le_cSup :=
343 assume (s : set ℝ) (a : ℝ) (_ : bdd_above s) (_ : a ∈ s),
id └─┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └───────┘ ┴
typ └─┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
344 show a ≤ Sup s,
id ┴ ┴ └─┘ ┴
src ┴ └─┘
typ ┴ ┴ └─┘ ┴
345 from le_Sup s ‹bdd_above s› ‹a ∈ s›,
id └────┘ ┴ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
src └────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
doc ┴└───────┘ ┴ ┴ ┴
346 cSup_le :=
347 assume (s : set ℝ) (a : ℝ) (_ : s.nonempty) (H : ∀b∈s, b ≤ a),
id └─┘ ┴ ┴ ┴└───────┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └───────┘ ┴
typ └─┘ ┴ ┴ ┴└───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
348 show Sup s ≤ a,
id └─┘ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴
349 from Sup_le_ub s ‹s.nonempty› H,
id └───────┘ ┴ ┴┴└───────┘┴ ┴
src └───────┘ ┴ └───────┘┴
typ └───────┘ ┴ ┴┴└───────┘┴ ┴
doc ┴ └───────┘┴
350 cInf_le :=
351 assume (s : set ℝ) (a : ℝ) (_ : bdd_below s) (_ : a ∈ s),
id └─┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └───────┘ ┴
typ └─┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
352 show Inf s ≤ a,
id └─┘ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴
353 from Inf_le s ‹bdd_below s› ‹a ∈ s›,
id └────┘ ┴ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
src └────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
doc ┴└───────┘ ┴ ┴ ┴
354 le_cInf :=
355 assume (s : set ℝ) (a : ℝ) (_ : s.nonempty) (H : ∀b∈s, a ≤ b),
id └─┘ ┴ ┴ ┴└───────┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └───────┘ ┴
typ └─┘ ┴ ┴ ┴└───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
356 show a ≤ Inf s,
id ┴ ┴ └─┘ ┴
src ┴ └─┘
typ ┴ ┴ └─┘ ┴
357 from lb_le_Inf s ‹s.nonempty› H,
id └───────┘ ┴ ┴┴└───────┘┴ ┴
src └───────┘ ┴ └───────┘┴
typ └───────┘ ┴ ┴┴└───────┘┴ ┴
doc ┴ └───────┘┴
358 decidable_le := classical.dec_rel _,
id └───────────────┘
src └───────────────┘
typ └───────────────┘
359 ..real.linear_order, ..real.lattice}
id └───────────────┘ └──────────┘
src └───────────────┘ └──────────┘
typ └───────────────┘ └──────────┘
360
361 theorem Sup_empty : lattice.Sup (∅ : set ℝ) = 0 := dif_neg $ by simp
id └─────────┘ ┴ └─┘ ┴ ┴ └─────┘
src └─────────┘ ┴ └─┘ ┴ ┴ └─────┘ └────
typ └─────────┘ ┴ └─┘ ┴ ┴ └─────┘ └────
doc └─────────┘ └────
txt └────
par └────
pid └
st └─────
362
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
363 theorem Sup_of_not_bdd_above {s : set ℝ} (hs : ¬ bdd_above s) : lattice.Sup s = 0 :=
id └─┘ ┴ ┴ └───────┘ ┴ └─────────┘ ┴ ┴
src └─┘ ┴ ┴ └───────┘ └─────────┘ ┴
typ └─┘ ┴ ┴ └───────┘ ┴ └─────────┘ ┴ ┴
doc └───────┘ └─────────┘
364 dif_neg $ assume h, hs h.2
id └─────┘ ┴ └┘ ┴┴
src └─────┘ ┴
typ └─────┘ ┴ └┘ ┴┴
365
366 theorem Sup_univ : real.Sup set.univ = 0 :=
id └──────┘ └──────┘ ┴
src └──────┘ └──────┘ ┴
typ └──────┘ └──────┘ ┴
367 real.Sup_of_not_bdd_above $ λ ⟨x, h⟩, not_le_of_lt (lt_add_one _) $ h (set.mem_univ _)
id └───────────────────────┘ ┴ ┴ └──────────┘ └────────┘ └──────────┘
src └───────────────────────┘ └──────────┘ └────────┘ └──────────┘
typ └───────────────────────┘ ┴ ┴ └──────────┘ └────────┘ └──────────┘
368
369 theorem Inf_empty : lattice.Inf (∅ : set ℝ) = 0 :=
id └─────────┘ ┴ └─┘ ┴ ┴
src └─────────┘ ┴ └─┘ ┴ ┴
typ └─────────┘ ┴ └─┘ ┴ ┴
doc └─────────┘
370 show Inf ∅ = 0, by simp [Inf]; exact Sup_empty
id └─┘ ┴ ┴ └─┘ └───────┘
src └─┘ ┴ ┴ └────┘└─┘┴ └────┘└───────┘└
typ └─┘ ┴ ┴ └────┘└─┘┴ └────┘└───────┘└
doc └────┘ ┴ └────┘ └
txt └────┘ ┴ └────┘ └
par └────┘ ┴ └────┘ └
pid ┴┴ ┴ ┴ └
st └────────────────────────────
371
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
372 theorem Inf_of_not_bdd_below {s : set ℝ} (hs : ¬ bdd_below s) : lattice.Inf s = 0 :=
id └─┘ ┴ ┴ └───────┘ ┴ └─────────┘ ┴ ┴
src └─┘ ┴ ┴ └───────┘ └─────────┘ ┴
typ └─┘ ┴ ┴ └───────┘ ┴ └─────────┘ ┴ ┴
doc └───────┘ └─────────┘
373 have bdd_above {x | -x ∈ s} → bdd_below s, from
id └───────┘ ┴┴ ┴┴ ┴ ┴ └───────┘ ┴
src └───────┘ ┴ ┴ ┴ └───────┘
typ └───────┘ ┴┴ ┴┴ ┴ ┴ └───────┘ ┴
doc └───────┘ └───────┘
374 assume ⟨b, hb⟩, ⟨-b, assume x hxs, neg_le.2 $ hb $ by simp [hxs]⟩,
id ┴┴ └┘ ┴ ┴ └─┘ └────┘┴ └─┘
src ┴ └────┘┴ └────┘ ┴
typ ┴┴ └┘ ┴ ┴ └─┘ └────┘┴ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────┘
375 have ¬ bdd_above {x | -x ∈ s}, from mt this hs,
id ┴ └───────┘ ┴┴ ┴┴ ┴ ┴ └┘ └──┘ └┘
src ┴ └───────┘ ┴ ┴ ┴ └┘
typ ┴ └───────┘ ┴┴ ┴┴ ┴ ┴ └┘ └──┘ └┘
doc └───────┘
376 neg_eq_zero.2 $ Sup_of_not_bdd_above $ this
id └─────────┘┴ └──────────────────┘ └──┘
src └─────────┘┴ └──────────────────┘
typ └─────────┘┴ └──────────────────┘ └──┘
377
378 theorem cau_seq_converges (f : cau_seq ℝ abs) : ∃ x, f ≈ const abs x :=
id └─────┘ ┴ └─┘ ┴ ┴┴ ┴ ┴ └───┘ └─┘ ┴
src └─────┘ ┴ └─┘ ┴ ┴ ┴ └───┘ └─┘
typ └─────┘ ┴ └─┘ ┴ ┴┴ ┴ ┴ └───┘ └─┘ ┴
doc └───┘
379 begin
st └─────
380 let S := {x : ℝ | const abs x < f},
id ┴ └───┘ └─┘ ┴ ┴
src └───────┘┴└──┘ └─┘└───┘┴└─┘┴ ┴┴┴ ┴
typ └───────┘┴└──┘ └─┘└───┘┴└─┘┴ ┴┴┴┴┴
doc └───────┘ └──┘ └─┘└───┘┴ ┴ ┴ ┴ ┴
txt └───────┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────┘└─
381 have lb : ∃ x, x ∈ S := exists_lt f,
id ┴ ┴ ┴ ┴ └───────┘ ┴
src └────────┘┴└┘┴┴ ┴┴┴ └──┘└───────┘┴
typ └────────┘┴└┘┴┴ ┴┴┴┴└──┘└───────┘┴┴
doc └────────┘ └┘ ┴ ┴ ┴ └──┘ ┴
txt └────────┘ └┘ ┴ ┴ ┴ └──┘ ┴
par └────────┘ └┘ ┴ ┴ ┴ └──┘ ┴
pid └─────┘└─┘ └┘ ┴ ┴ ┴ └──┘ ┴
st ────────────────────────────────────┘└─
382 have ub' : ∀ x, f < const abs x → ∀ y ∈ S, y ≤ x :=
id ┴ ┴ └───┘ └─┘ ┴ ┴
src └─────────┘ └┘ ┴ ┴ ┴└───┘┴└─┘┴ ┴ ┴ └───┘ ┴ ┴┴┴ └───
typ └─────────┘ └┘ ┴┴┴┴┴└───┘┴└─┘┴ ┴ ┴ └───┘┴ ┴ ┴┴┴ └───
doc └─────────┘ └┘ ┴ ┴ ┴└───┘┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───
txt └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───
par └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───
pid └──────┘└─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───
st ──────────────────────────────────────────────────────
383 λ x h y yS, le_of_lt $ const_lt.1 $ cau_seq.lt_trans yS h,
id └──────┘ └──────┘ └──────────────┘
src ───┘ └─────────┘└──────┘┴ ┴└──────┘└─┘ ┴└──────────────┘┴ ┴
typ ───┘ └─────────┘└──────┘┴ ┴└──────┘└─┘ ┴└──────────────┘┴ ┴
doc ───┘ └─────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
txt ───┘ └─────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
par ───┘ └─────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
pid ───┘ └─────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────┘└─
384 have ub : ∃ x, ∀ y ∈ S, y ≤ x := (exists_gt f).imp ub',
id ┴ ┴ ┴ └───────┘ ┴ └─┘
src └────────┘┴└┘┴┴ └───┘ ┴ ┴ ┴ └──┘ └───────┘┴ └────┘
typ └────────┘┴└┘┴┴ └───┘┴ ┴ ┴ ┴ └──┘ └───────┘┴┴└────┘└─┘
doc └────────┘ └┘ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴ └────┘
txt └────────┘ └┘ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴ └────┘
par └────────┘ └┘ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴ └────┘
pid └─────┘└─┘ └┘ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴ └────┘
st ───────────────────────────────────────────────────────┘└─
385 refine ⟨Sup S,
id └─┘ ┴
src └─────┘ └─┘┴ └─
typ └─────┘ └─┘┴┴└─
doc └─────┘ ┴ └─
txt └─────┘ ┴ └─
par └─────┘ ┴ └─
pid ┴ ┴ └─
st ─────────────────
386 ((lt_total _ _).resolve_left (λ h, _)).resolve_right (λ h, _)⟩,
id └──────┘
src ───┘ └──────┘└─────────────────┘ └────────────────────┘ └─────┘
typ ───┘ └──────┘└─────────────────┘ └────────────────────┘ └─────┘
doc ───┘ └─────────────────┘ └────────────────────┘ └─────┘
txt ───┘ └─────────────────┘ └────────────────────┘ └─────┘
par ───┘ └─────────────────┘ └────────────────────┘ └─────┘
pid ───┘ └─────────────────┘ └────────────────────┘ └─────┘
st ─────────────────────────────────────────────────────────────────┘└─
387 { rcases h with ⟨ε, ε0, i, ih⟩,
id ┴
src └─────┘ └──────────────────┘
typ └─────┘┴└──────────────────┘
doc └─────┘ └──────────────────┘
txt └─────┘ └──────────────────┘
par └─────┘ └──────────────────┘
pid ┴ └──────────────────┘
st ───┘└──────────────────────────┘└─
388 refine not_lt_of_le (Sup_le_ub S lb (ub' _ _))
id └──────────┘ └───────┘ ┴ └┘ └─┘
src └─────┘└──────────┘┴ └───────┘┴ ┴ ┴ └──────
typ └─────┘└──────────┘┴ └───────┘┴┴┴└┘┴ └─┘└──────
doc └─────┘ ┴ ┴ ┴ ┴ └──────
txt └─────┘ ┴ ┴ ┴ ┴ └──────
par └─────┘ ┴ ┴ ┴ ┴ └──────
pid ┴ ┴ ┴ ┴ ┴ └──────
st ───────────────────────────────────────────────────
389 ((sub_lt_self_iff _).2 (half_pos ε0)),
id └─────────────┘ └──────┘ └┘
src ─────┘ └─────────────┘└────┘ └──────┘┴ └┘
typ ─────┘ └─────────────┘└────┘ └──────┘┴└┘└┘
doc ─────┘ └────┘ ┴ └┘
txt ─────┘ └────┘ ┴ └┘
par ─────┘ └────┘ ┴ └┘
pid ─────┘ └────┘ ┴ └┘
st ──────────────────────────────────────────┘└─
390 refine ⟨_, half_pos ε0, i, λ j ij, _⟩,
id └──────┘ └┘ ┴
src └─────┘ └─┘└──────┘┴ └┘ └┘ └───────┘
typ └─────┘ └─┘└──────┘┴└┘└┘┴└┘ └───────┘
doc └─────┘ └─┘ ┴ └┘ └┘ └───────┘
txt └─────┘ └─┘ ┴ └┘ └┘ └───────┘
par └─────┘ └─┘ ┴ └┘ └┘ └───────┘
pid ┴ └─┘ ┴ └┘ └┘ └───────┘
st ────────────────────────────────────────┘└─
391 rw [sub_apply, const_apply, sub_right_comm,
id └───────┘ └─────────┘ └────────────┘
src └──┘└───────┘└┘└─────────┘└┘└────────────┘└─
typ └──┘└───────┘└┘└─────────┘└┘└────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ └─
st ────────────────┘└───────────┘└──────────────┘└─
392 le_sub_iff_add_le, add_halves],
id └───────────────┘ └────────┘
src ─────┘└───────────────┘└┘└────────┘┴
typ ─────┘└───────────────┘└┘└────────┘┴
doc ─────┘ └┘ ┴
txt ─────┘ └┘ ┴
par ─────┘ └┘ ┴
pid ─────┘ └┘ ┴
st ──────────────────────┘└──────────┘└──
393 exact ih _ ij },
id └┘ └┘
src └────┘ └─┘ ┴
typ └────┘└┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────┘└┘└
394 { rcases h with ⟨ε, ε0, i, ih⟩,
id ┴
src └─────┘ └──────────────────┘
typ └─────┘┴└──────────────────┘
doc └─────┘ └──────────────────┘
txt └─────┘ └──────────────────┘
par └─────┘ └──────────────────┘
pid ┴ └──────────────────┘
st ───────────────────────────────┘└─
395 refine not_lt_of_le (le_Sup S ub _)
id └──────────┘ └────┘ ┴ └┘
src └─────┘└──────────┘┴ └────┘┴ ┴ └───
typ └─────┘└──────────┘┴ └────┘┴┴┴└┘└───
doc └─────┘ ┴ ┴ ┴ └───
txt └─────┘ ┴ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ └───
pid ┴ ┴ ┴ ┴ └───
st ────────────────────────────────────────
396 ((lt_add_iff_pos_left _).2 (half_pos ε0)),
id └─────────────────┘ └──────┘ └┘
src ─────┘ └─────────────────┘└────┘ └──────┘┴ └┘
typ ─────┘ └─────────────────┘└────┘ └──────┘┴└┘└┘
doc ─────┘ └────┘ ┴ └┘
txt ─────┘ └────┘ ┴ └┘
par ─────┘ └────┘ ┴ └┘
pid ─────┘ └────┘ ┴ └┘
st ──────────────────────────────────────────────┘└─
397 refine ⟨_, half_pos ε0, i, λ j ij, _⟩,
id └──────┘ └┘ ┴
src └─────┘ └─┘└──────┘┴ └┘ └┘ └───────┘
typ └─────┘ └─┘└──────┘┴└┘└┘┴└┘ └───────┘
doc └─────┘ └─┘ ┴ └┘ └┘ └───────┘
txt └─────┘ └─┘ ┴ └┘ └┘ └───────┘
par └─────┘ └─┘ ┴ └┘ └┘ └───────┘
pid ┴ └─┘ ┴ └┘ └┘ └───────┘
st ────────────────────────────────────────┘└─
398 rw [sub_apply, const_apply, add_comm, ← sub_sub,
id └───────┘ └─────────┘ └──────┘ └─────┘
src └──┘└───────┘└┘└─────────┘└┘└──────┘└──┘└─────┘└─
typ └──┘└───────┘└┘└─────────┘└┘└──────┘└──┘└─────┘└─
doc └──┘ └┘ └┘ └──┘ └─
txt └──┘ └┘ └┘ └──┘ └─
par └──┘ └┘ └┘ └──┘ └─
pid └┘ └┘ └┘ └──┘ └─
st ────────────────┘└───────────┘└────────┘└─────────┘└─
399 le_sub_iff_add_le, add_halves],
id └───────────────┘ └────────┘
src ─────┘└───────────────┘└┘└────────┘┴
typ ─────┘└───────────────┘└┘└────────┘┴
doc ─────┘ └┘ ┴
txt ─────┘ └┘ ┴
par ─────┘ └┘ ┴
pid ─────┘ └┘ ┴
st ──────────────────────┘└──────────┘└──
400 exact ih _ ij }
id └┘ └┘
src └────┘ └─┘ ┴
typ └────┘└┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────┘└─
401 end
st ──┘
402
403 noncomputable instance : cau_seq.is_complete ℝ abs := ⟨cau_seq_converges⟩
id └─────────────────┘ ┴ └─┘ └───────────────┘
src └─────────────────┘ ┴ └─┘ └───────────────┘
typ └─────────────────┘ ┴ └─┘ └───────────────┘
404
405 theorem sqrt_exists : ∀ {x : ℝ}, 0 ≤ x → ∃ y, 0 ≤ y ∧ y * y = x :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
406 suffices H : ∀ {x : ℝ}, 0 < x → x ≤ 1 → ∃ y, 0 < y ∧ y * y = x, begin
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └─────
407 intros x x0, cases x0,
id └┘
src └─────────┘ └────┘
typ └─────────┘ └────┘└┘
doc └─────────┘ └────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
pid └───┘ ┴
st ────────────┘└────────┘└─
408 cases le_total x 1 with x1 x1,
id └──────┘ ┴
src └────┘└──────┘┴ └───────────┘
typ └────┘└──────┘┴┴└───────────┘
doc └────┘ ┴ └───────────┘
txt └────┘ ┴ └───────────┘
par └────┘ ┴ └───────────┘
pid ┴ ┴ ┴└──────────┘
st ──────────────────────────────┘└─
409 { rcases H x0 x1 with ⟨y, y0, hy⟩,
id ┴ └┘ └┘
src └─────┘ ┴ ┴ └───────────────┘
typ └─────┘┴┴└┘┴└┘└───────────────┘
doc └─────┘ ┴ ┴ └───────────────┘
txt └─────┘ ┴ ┴ └───────────────┘
par └─────┘ ┴ ┴ └───────────────┘
pid ┴ ┴ ┴ └───────────────┘
st ───┘└─────────────────────────────┘└─
410 exact ⟨y, le_of_lt y0, hy⟩ },
id ┴ └──────┘ └┘ └┘
src └────┘ └┘└──────┘┴ └┘ └┘
typ └────┘ ┴└┘└──────┘┴└┘└┘└┘└┘
doc └────┘ └┘ ┴ └┘ └┘
txt └────┘ └┘ ┴ └┘ └┘
par └────┘ └┘ ┴ └┘ └┘
pid ┴ └┘ ┴ └┘ ┴┴
st ──────────────────────────────┘└┘└
411 { have := (inv_le_inv x0 zero_lt_one).2 x1,
id └────────┘ └┘ └─────────┘ └┘
src └──────┘ └────────┘┴ ┴└─────────┘└──┘
typ └──────┘ └────────┘┴└┘┴└─────────┘└──┘└┘
doc └──────┘ ┴ ┴ └──┘
txt └──────┘ ┴ ┴ └──┘
par └──────┘ ┴ ┴ └──┘
pid └───┘└─┘ ┴ ┴ └──┘
st ───┘└──────────────────────────────────────┘└─
412 rw inv_one at this,
id └─────┘
src └─┘└─────┘└──────┘
typ └─┘└─────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ─────────────────────┘└─
413 rcases H (inv_pos x0) this with ⟨y, y0, hy⟩,
id ┴ └─────┘ └┘ └──┘
src └─────┘ ┴ └─────┘┴ └┘ └───────────────┘
typ └─────┘┴┴ └─────┘┴└┘└┘└──┘└───────────────┘
doc └─────┘ ┴ ┴ └┘ └───────────────┘
txt └─────┘ ┴ ┴ └┘ └───────────────┘
par └─────┘ ┴ ┴ └┘ └───────────────┘
pid ┴ ┴ ┴ └┘ └───────────────┘
st ──────────────────────────────────────────────┘└─
414 refine ⟨y⁻¹, le_of_lt (inv_pos y0), _⟩, rw [← mul_inv', hy, inv_inv'] },
id ┴└┘ └──────┘ └─────┘ └┘ └──────┘ └┘ └──────┘
src └─────┘ └┘└┘└──────┘┴ └─────┘┴ └───┘ └────┘└──────┘└┘ └┘└──────┘└┘
typ └─────┘ ┴└┘└┘└──────┘┴ └─────┘┴└┘└───┘ └────┘└──────┘└┘└┘└┘└──────┘└┘
doc └─────┘ └┘ ┴ ┴ └───┘ └────┘ └┘ └┘ └┘
txt └─────┘ └┘ ┴ ┴ └───┘ └────┘ └┘ └┘ └┘
par └─────┘ └┘ ┴ ┴ └───┘ └────┘ └┘ └┘ └┘
pid ┴ └┘ ┴ ┴ └───┘ └──┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────┘└──────────────┘└──┘└────────┘┴┴└┘└
415 { exact ⟨0, by simp [x0.symm]⟩ }
src └────┘ └─┘ ┴└────┘ ┴└┘
typ └────┘ └─┘ ┴└────┘└─────┘┴└┘
doc └────┘ └─┘ ┴└────┘ ┴└┘
txt └────┘ └─┘ ┴└────┘ ┴└┘
par └────┘ └─┘ ┴└────┘ ┴└┘
pid ┴ └─┘ └─────┘ └┘┴
st ───────────────┘└─────────────┘└┘└─
416 end,
st ──┘
417 λ x x0 x1, begin
id ┴ └┘ └┘
typ ┴ └┘ └┘
st └─────
418 let S := {y | 0 < y ∧ y * y ≤ x},
id ┴ ┴ ┴ ┴ ┴
src └───────┘┴└────┘┴┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴
typ └───────┘┴└────┘┴┴ ┴ ┴ ┴┴┴ ┴┴┴┴┴
doc └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└─
419 have lb : x ∈ S := ⟨x0, by simpa using (mul_le_mul_right x0).2 x1⟩,
id ┴ ┴ ┴ └┘ └──────────────┘ └┘ └┘
src └────────┘ ┴┴┴ └──┘ └┘ ┴└──────────┘ └──────────────┘┴ └──┘ ┴
typ └────────┘┴┴┴┴┴└──┘ └┘└┘ ┴└──────────┘ └──────────────┘┴└┘└──┘└┘┴
doc └────────┘ ┴ ┴ └──┘ └┘ ┴└──────────┘ ┴ └──┘ ┴
txt └────────┘ ┴ ┴ └──┘ └┘ ┴└──────────┘ ┴ └──┘ ┴
par └────────┘ ┴ ┴ └──┘ └┘ ┴└──────────┘ ┴ └──┘ ┴
pid └─────┘└─┘ ┴ ┴ └──┘ └┘ └───────────┘ ┴ └──┘ ┴
st ───────────────────────────┘└─────────────────────────────────────┘┴└─
420 have ub : ∀ y ∈ S, (y:ℝ) ≤ 1,
id ┴
src └────────┘ └───┘ ┴ ┴ └┘ └┘
typ └────────┘ └───┘┴ ┴ ┴ └┘ └┘
doc └────────┘ └───┘ ┴ ┴ └┘ └┘
txt └────────┘ └───┘ ┴ ┴ └┘ └┘
par └────────┘ └───┘ ┴ ┴ └┘ └┘
pid └─────┘└─┘ └───┘ ┴ ┴ └┘ ┴┴
st ─────────────────────────────┘└─
421 { intros y yS, cases yS with y0 yx,
id └┘
src └─────────┘ └────┘ └─────────┘
typ └─────────┘ └────┘└┘└─────────┘
doc └─────────┘ └────┘ └─────────┘
txt └─────────┘ └────┘ └─────────┘
par └─────────┘ └────┘ └─────────┘
pid └───┘ ┴ └─────────┘
st ───┘└─────────┘└───────────────────┘└─
422 refine (mul_self_le_mul_self_iff (le_of_lt y0) zero_le_one).2 _,
id └──────────────────────┘ └──────┘ └┘ └─────────┘
src └─────┘ └──────────────────────┘┴ └──────┘┴ └┘└─────────┘└───┘
typ └─────┘ └──────────────────────┘┴ └──────┘┴└┘└┘└─────────┘└───┘
doc └─────┘ ┴ ┴ └┘ └───┘
txt └─────┘ ┴ ┴ └┘ └───┘
par └─────┘ ┴ ┴ └┘ └───┘
pid ┴ ┴ ┴ └┘ └───┘
st ──────────────────────────────────────────────────────────────────┘└─
423 simpa using le_trans yx x1 },
id └──────┘ └┘ └┘
src └──────────┘└──────┘┴ ┴ ┴
typ └──────────┘└──────┘┴└┘┴└┘┴
doc └──────────┘ ┴ ┴ ┴
txt └──────────┘ ┴ ┴ ┴
par └──────────┘ ┴ ┴ ┴
pid ┴└────┘ ┴ ┴ ┴
st ──────────────────────────────┘└┘└
424 have S0 : 0 < Sup S := lt_of_lt_of_le x0 (le_Sup _ ⟨_, ub⟩ lb),
id └─┘ ┴ └────────────┘ └┘ └────┘ └┘ └┘
src └──────────┘ ┴└─┘┴ └──┘└────────────┘┴ ┴ └────┘└─┘ └─┘ └┘ ┴
typ └──────────┘ ┴└─┘┴┴└──┘└────────────┘┴└┘┴ └────┘└─┘ └─┘└┘└┘└┘┴
doc └──────────┘ ┴ ┴ └──┘ ┴ ┴ └─┘ └─┘ └┘ ┴
txt └──────────┘ ┴ ┴ └──┘ ┴ ┴ └─┘ └─┘ └┘ ┴
par └──────────┘ ┴ ┴ └──┘ ┴ ┴ └─┘ └─┘ └┘ ┴
pid └─────┘└───┘ ┴ ┴ └──┘ ┴ ┴ └─┘ └─┘ └┘ ┴
st ───────────────────────────────────────────────────────────────┘└─
425 refine ⟨Sup S, S0, le_antisymm (not_lt.1 $ λ h, _) (not_lt.1 $ λ h, _)⟩,
id └─┘ ┴ └┘ └─────────┘ └────┘
src └─────┘ └─┘┴ └┘ └┘└─────────┘┴ └─┘ ┴ └─────┘ └────┘└─┘ ┴ └─────┘
typ └─────┘ └─┘┴┴└┘└┘└┘└─────────┘┴ └─┘ ┴ └─────┘ └────┘└─┘ ┴ └─────┘
doc └─────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └─────┘ └─┘ ┴ └─────┘
txt └─────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └─────┘ └─┘ ┴ └─────┘
par └─────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └─────┘ └─┘ ┴ └─────┘
pid ┴ ┴ └┘ └┘ ┴ └─┘ ┴ └─────┘ └─┘ ┴ └─────┘
st ────────────────────────────────────────────────────────────────────────┘└─
426 { rw [← div_lt_iff S0, lt_Sup S ⟨_, lb⟩ ⟨_, ub⟩] at h,
id └────────┘ └┘ └────┘ ┴ └┘ └┘
src └────┘└────────┘┴ └┘└────┘┴ ┴ └─┘ └┘ └─┘ └─────┘
typ └────┘└────────┘┴└┘└┘└────┘┴┴┴ └─┘└┘└┘ └─┘└┘└─────┘
doc └────┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └─────┘
txt └────┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └─────┘
par └────┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └─────┘
pid └──┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └┘└───┘
st ───┘└─────────────────┘└────────────────────────┘┴└───┘└─
427 rcases h with ⟨y, ⟨y0, yx⟩, hy⟩,
id ┴
src └─────┘ └─────────────────────┘
typ └─────┘┴└─────────────────────┘
doc └─────┘ └─────────────────────┘
txt └─────┘ └─────────────────────┘
par └─────┘ └─────────────────────┘
pid ┴ └─────────────────────┘
st ──────────────────────────────────┘└─
428 rw [div_lt_iff S0, ← div_lt_iff' y0, lt_Sup S ⟨_, lb⟩ ⟨_, ub⟩] at hy,
id └────────┘ └┘ └─────────┘ └┘ └────┘ ┴ └┘ └┘
src └──┘└────────┘┴ └──┘└─────────┘┴ └┘└────┘┴ ┴ └─┘ └┘ └─┘ └──────┘
typ └──┘└────────┘┴└┘└──┘└─────────┘┴└┘└┘└────┘┴┴┴ └─┘└┘└┘ └─┘└┘└──────┘
doc └──┘ ┴ └──┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └──────┘
txt └──┘ ┴ └──┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └──────┘
par └──┘ ┴ └──┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └──────┘
pid └┘ ┴ └──┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └┘└────┘
st ────────────────────┘└────────────────┘└────────────────────────┘┴└────┘└─
429 rcases hy with ⟨z, ⟨z0, zx⟩, hz⟩,
id └┘
src └─────┘ └─────────────────────┘
typ └─────┘└┘└─────────────────────┘
doc └─────┘ └─────────────────────┘
txt └─────┘ └─────────────────────┘
par └─────┘ └─────────────────────┘
pid ┴ └─────────────────────┘
st ───────────────────────────────────┘└─
430 rw [div_lt_iff y0] at hz,
id └────────┘ └┘
src └──┘└────────┘┴ └─────┘
typ └──┘└────────┘┴└┘└─────┘
doc └──┘ ┴ └─────┘
txt └──┘ ┴ └─────┘
par └──┘ ┴ └─────┘
pid └┘ ┴ ┴└────┘
st ────────────────────┘┴└────┘└─
431 exact not_lt_of_lt
id └──────────┘
src └────┘└──────────┘└
typ └────┘└──────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ───────────────────────
432 ((mul_lt_mul_right y0).1 (lt_of_le_of_lt yx hz))
id └──────────────┘ └┘ └┘
src ─────┘ └──────────────┘┴ └──┘ ┴ ┴ └──
typ ─────┘ └──────────────┘┴└┘└──┘ ┴└┘┴ └──
doc ─────┘ ┴ └──┘ ┴ ┴ └──
txt ─────┘ ┴ └──┘ ┴ ┴ └──
par ─────┘ ┴ └──┘ ┴ ┴ └──
pid ─────┘ ┴ └──┘ ┴ ┴ └──
st ───────────────────────────────────────────────────────
433 ((mul_lt_mul_left z0).1 (lt_of_le_of_lt zx hz)) },
id └─────────────┘ └┘ └────────────┘ └┘ └┘
src ─────┘ └─────────────┘┴ └──┘ └────────────┘┴ ┴ └─┘
typ ─────┘ └─────────────┘┴└┘└──┘ └────────────┘┴└┘┴└┘└─┘
doc ─────┘ ┴ └──┘ ┴ ┴ └─┘
txt ─────┘ ┴ └──┘ ┴ ┴ └─┘
par ─────┘ ┴ └──┘ ┴ ┴ └─┘
pid ─────┘ ┴ └──┘ ┴ ┴ └┘┴
st ─────────────────────────────────────────────────────┘└┘└
434 { let s := Sup S, let y := s + (x - s * s) / 3,
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘└─┘┴ └───────┘ ┴┴┴ ┴┴┴ ┴ ┴ └┘┴└┘
typ └───────┘└─┘┴┴ └───────┘ ┴┴┴ ┴┴┴┴ ┴ ┴┴└┘┴└┘
doc └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
txt └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
par └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
pid └───┘┴└─┘ ┴ └───┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴
st ─────────────────┘└────────────────────────────┘└─
435 replace h : 0 < x - s * s := sub_pos.2 h,
id ┴ ┴ └─────┘ ┴
src └────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘└─────┘└─┘
typ └────────────┘ ┴┴┴ ┴ ┴ ┴┴└──┘└─────┘└─┘┴
doc └────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘
txt └────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘
par └────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘
pid └┘└───┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘
st ───────────────────────────────────────────┘└─
436 have _30 := bit1_pos zero_le_one,
id └──────┘ └─────────┘
src └──────────┘└──────┘┴└─────────┘
typ └──────────┘└──────┘┴└─────────┘
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid └──────┘┴└─┘ ┴
st ───────────────────────────────────┘└─
437 have : s < y := (lt_add_iff_pos_right _).2 (div_pos h _30),
id ┴ ┴ └──────────────────┘ └─────┘ ┴ └─┘
src └─────┘ ┴ ┴ └──┘ └──────────────────┘└────┘ └─────┘┴ ┴ ┴
typ └─────┘┴┴ ┴┴└──┘ └──────────────────┘└────┘ └─────┘┴┴┴└─┘┴
doc └─────┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
438 refine not_le_of_lt this (le_Sup S ⟨_, ub⟩ ⟨lt_trans S0 this, _⟩),
id └──────────┘ └────┘ ┴ └┘ └──────┘ └┘ └──┘
src └─────┘└──────────┘┴ ┴ └────┘┴ ┴ └─┘ └┘ └──────┘┴ ┴ └───┘
typ └─────┘└──────────┘┴ ┴ └────┘┴┴┴ └─┘└┘└┘ └──────┘┴└┘┴└──┘└───┘
doc └─────┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └───┘
par └─────┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └───┘
st ────────────────────────────────────────────────────────────────────┘└─
439 rw [add_mul_self_eq, add_assoc, ← le_sub_iff_add_le', ← add_mul,
id └─────────────┘ └───────┘ └────────────────┘ └─────┘
src └──┘└─────────────┘└┘└───────┘└──┘└────────────────┘└──┘└─────┘└─
typ └──┘└─────────────┘└┘└───────┘└──┘└────────────────┘└──┘└─────┘└─
doc └──┘ └┘ └──┘ └──┘ └─
txt └──┘ └┘ └──┘ └──┘ └─
par └──┘ └┘ └──┘ └──┘ └─
pid └┘ └┘ └──┘ └──┘ └─
st ──────────────────────┘└─────────┘└────────────────────┘└─────────┘└─
440 ← le_div_iff (div_pos h _30), div_div_cancel (ne_of_gt h)],
id └────────┘ └─────┘ ┴ └─┘ └────────────┘ └──────┘ ┴
src ───────┘└────────┘┴ └─────┘┴ ┴ └─┘└────────────┘┴ └──────┘┴ └┘
typ ───────┘└────────┘┴ └─────┘┴┴┴└─┘└─┘└────────────┘┴ └──────┘┴┴└┘
doc ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
txt ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
par ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
pid ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
st ─────────────────────────────────┘└───────────────────────────┘└──
441 apply add_le_add,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
442 { simpa using (mul_le_mul_left (@two_pos ℝ _)).2 (Sup_le_ub _ ⟨_, lb⟩ ub) },
id └─────────────┘ └─────┘ └───────┘ └┘ └┘
src └──────────┘ └─────────────┘┴ └─────┘┴ └─────┘ └───────┘└─┘ └─┘ └┘ └┘
typ └──────────┘ └─────────────┘┴ └─────┘┴ └─────┘ └───────┘└─┘ └─┘└┘└┘└┘└┘
doc └──────────┘ ┴ ┴ └─────┘ └─┘ └─┘ └┘ └┘
txt └──────────┘ ┴ ┴ └─────┘ └─┘ └─┘ └┘ └┘
par └──────────┘ ┴ ┴ └─────┘ └─┘ └─┘ └┘ └┘
pid ┴└────┘ ┴ ┴ └─────┘ └─┘ └─┘ └┘ ┴┴
st ─────┘└──────────────────────────────────────────────────────────────────────┘└┘└
443 { rw [div_le_one_iff_le _30],
id └───────────────┘ └─┘
src └──┘└───────────────┘┴ ┴
typ └──┘└───────────────┘┴└─┘┴
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid └┘ ┴ ┴
st ──────────────────────────────┘└──
444 refine le_trans (sub_le_self _ (mul_self_nonneg _)) (le_trans x1 _),
id └─────────┘ └─────────────┘ └──────┘ └┘
src └─────┘ ┴ └─────────┘└─┘ └─────────────┘└───┘ └──────┘┴ └─┘
typ └─────┘ ┴ └─────────┘└─┘ └─────────────┘└───┘ └──────┘┴└┘└─┘
doc └─────┘ ┴ └─┘ └───┘ ┴ └─┘
txt └─────┘ ┴ └─┘ └───┘ ┴ └─┘
par └─────┘ ┴ └─┘ └───┘ ┴ └─┘
pid ┴ ┴ └─┘ └───┘ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
445 exact (le_add_iff_nonneg_left _).2 (le_of_lt two_pos) } }
id └────────────────────┘ └──────┘ └─────┘
src └────┘ └────────────────────┘└────┘ └──────┘┴└─────┘└┘
typ └────┘ └────────────────────┘└────┘ └──────┘┴└─────┘└┘
doc └────┘ └────┘ ┴ └┘
txt └────┘ └────┘ ┴ └┘
par └────┘ └────┘ ┴ └┘
pid ┴ └────┘ ┴ ┴┴
st ───────────────────────────────────────────────────────────┘└───
446 end
st ──┘
447
448 def sqrt_aux (f : cau_seq ℚ abs) : ℕ → ℚ
id └─────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴
doc ┴ ┴
449 | 0 := rat.mk_nat (f 0).num.to_nat.sqrt (f 0).denom.sqrt
id └────────┘ ┴ └─┘ └────┘ └──┘ ┴ └───┘ └──┘
src └────────┘ └─┘ └────┘ └──┘ └───┘ └──┘
typ └────────┘ ┴ └─┘ └────┘ └──┘ ┴ └───┘ └──┘
doc └────────┘ └──┘ └──┘
450 | (n + 1) := let s := sqrt_aux n in max 0 $ (s + f (n+1) / s) / 2
id ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
451
452 theorem sqrt_aux_nonneg (f : cau_seq ℚ abs) : ∀ i : ℕ, 0 ≤ sqrt_aux f i
id └─────┘ ┴ └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴ └──────┘
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc ┴
453 | 0 := by rw [sqrt_aux, mk_nat_eq, mk_eq_div];
id └──────┘ └───────┘ └───────┘
src └──┘└──────┘└┘└───────┘└┘└───────┘┴
typ └──┘└──────┘└┘└───────┘└┘└───────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └───────────┘└─────────┘└─────────┘┴└─
454 apply div_nonneg'; exact int.cast_nonneg.2 (int.of_nat_nonneg _)
id └─────────┘ └─────────────┘ └───────────────┘
src └────┘└─────────┘ └────┘└─────────────┘└─┘ └───────────────┘└──┘
typ └────┘└─────────┘ └────┘└─────────────┘└─┘ └───────────────┘└──┘
doc └────┘ └────┘ └─┘ └──┘
txt └────┘ └────┘ └─┘ └──┘
par └────┘ └────┘ └─┘ └──┘
pid ┴ ┴ └─┘ └─┘┴
st ──────────────────────────────────────────────────────────────────┘
455 | (n + 1) := le_max_left _ _
id ┴ └─────────┘
src ┴ └─────────┘
typ ┴ └─────────┘
456
457 /- TODO(Mario): finish the proof
458 theorem sqrt_aux_converges (f : cau_seq ℚ abs) : ∃ h x, 0 ≤ x ∧ x * x = max 0 (mk f) ∧
459 mk ⟨sqrt_aux f, h⟩ = x :=
460 begin
461 rcases sqrt_exists (le_max_left 0 (mk f)) with ⟨x, x0, hx⟩,
462 suffices : ∃ h, mk ⟨sqrt_aux f, h⟩ = x,
463 { exact this.imp (λ h e, ⟨x, x0, hx, e⟩) },
464 apply of_near,
465
466 suffices : ∃ δ > 0, ∀ i, abs (↑(sqrt_aux f i) - x) < δ / 2 ^ i,
467 { rcases this with ⟨δ, δ0, hδ⟩,
468 intros,
469 }
470 end -/
471
472 noncomputable def sqrt (x : ℝ) : ℝ :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
473 classical.some (sqrt_exists (le_max_left 0 x))
id └────────────┘ └─────────┘ └─────────┘ ┴
src └────────────┘ └─────────┘ └─────────┘
typ └────────────┘ └─────────┘ └─────────┘ ┴
474 /-quotient.lift_on x
475 (λ f, mk ⟨sqrt_aux f, (sqrt_aux_converges f).fst⟩)
476 (λ f g e, begin
477 rcases sqrt_aux_converges f with ⟨hf, x, x0, xf, xs⟩,
478 rcases sqrt_aux_converges g with ⟨hg, y, y0, yg, ys⟩,
479 refine xs.trans (eq.trans _ ys.symm),
480 rw [← @mul_self_inj_of_nonneg ℝ _ x y x0 y0, xf, yg],
481 congr' 1, exact quotient.sound e
482 end)-/
483
484 theorem sqrt_prop (x : ℝ) : 0 ≤ sqrt x ∧ sqrt x * sqrt x = max 0 x :=
id ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴
src ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └─┘
typ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴
485 classical.some_spec (sqrt_exists (le_max_left 0 x))
id └─────────────────┘ └─────────┘ └─────────┘ ┴
src └─────────────────┘ └─────────┘ └─────────┘
typ └─────────────────┘ └─────────┘ └─────────┘ ┴
486 /-quotient.induction_on x $ λ f,
487 by rcases sqrt_aux_converges f with ⟨hf, _, x0, xf, rfl⟩; exact ⟨x0, xf⟩-/
488
489 theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0 :=
id ┴ ┴ └──┘ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ └──┘ ┴ ┴
490 eq_zero_of_mul_self_eq_zero $ (sqrt_prop x).2.trans $ max_eq_left h
id └─────────────────────────┘ └───────┘ ┴ ┴ └───┘ └─────────┘ ┴
src └─────────────────────────┘ └───────┘ ┴ └───┘ └─────────┘
typ └─────────────────────────┘ └───────┘ ┴ ┴ └───┘ └─────────┘ ┴
491
492 theorem sqrt_nonneg (x : ℝ) : 0 ≤ sqrt x := (sqrt_prop x).1
id ┴ ┴ └──┘ ┴ └───────┘ ┴ ┴
src ┴ ┴ └──┘ └───────┘ ┴
typ ┴ ┴ └──┘ ┴ └───────┘ ┴ ┴
493
494 @[simp] theorem mul_self_sqrt (h : 0 ≤ x) : sqrt x * sqrt x = x :=
id ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ └──┘ ┴ └──┘ ┴
typ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
495 (sqrt_prop x).2.trans (max_eq_right h)
id └───────┘ ┴ ┴ └───┘ └──────────┘ ┴
src └───────┘ ┴ └───┘ └──────────┘
typ └───────┘ ┴ ┴ └───┘ └──────────┘ ┴
496
497 @[simp] theorem sqrt_mul_self (h : 0 ≤ x) : sqrt (x * x) = x :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
498 (mul_self_inj_of_nonneg (sqrt_nonneg _) h).1 (mul_self_sqrt (mul_self_nonneg _))
id └────────────────────┘ └─────────┘ ┴ ┴ └───────────┘ └─────────────┘
src └────────────────────┘ └─────────┘ ┴ └───────────┘ └─────────────┘
typ └────────────────────┘ └─────────┘ ┴ ┴ └───────────┘ └─────────────┘
499
500 theorem sqrt_eq_iff_mul_self_eq (hx : 0 ≤ x) (hy : 0 ≤ y) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
501 sqrt x = y ↔ y * y = x :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
502 ⟨λ h, by rw [← h, mul_self_sqrt hx],
id ┴ ┴ └───────────┘ └┘
src └────┘ └┘└───────────┘┴ ┴
typ ┴ └────┘┴└┘└───────────┘┴└┘┴
doc └────┘ └┘ ┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid └──┘ └┘ ┴ ┴
st └──────┘└────────────────┘┴
503 λ h, by rw [← h, sqrt_mul_self hy]⟩
id ┴ ┴ └───────────┘ └┘
src └────┘ └┘└───────────┘┴ ┴
typ ┴ └────┘┴└┘└───────────┘┴└┘┴
doc └────┘ └┘ ┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid └──┘ └┘ ┴ ┴
st └──────┘└────────────────┘┴
504
505 @[simp] theorem sqr_sqrt (h : 0 ≤ x) : sqrt x ^ 2 = x :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
506 by rw [pow_two, mul_self_sqrt h]
id └─────┘ └───────────┘ ┴
src └──┘└─────┘└┘└───────────┘┴ └─
typ └──┘└─────┘└┘└───────────┘┴┴└─
doc └──┘ └┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └──────────┘└───────────────┘┴└
507
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
508 @[simp] theorem sqrt_sqr (h : 0 ≤ x) : sqrt (x ^ 2) = x :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
509 by rw [pow_two, sqrt_mul_self h]
id └─────┘ └───────────┘ ┴
src └──┘└─────┘└┘└───────────┘┴ └─
typ └──┘└─────┘└┘└───────────┘┴┴└─
doc └──┘ └┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └──────────┘└───────────────┘┴└
510
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
511 theorem sqrt_eq_iff_sqr_eq (hx : 0 ≤ x) (hy : 0 ≤ y) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
512 sqrt x = y ↔ y ^ 2 = x :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
513 by rw [pow_two, sqrt_eq_iff_mul_self_eq hx hy]
id └─────┘ └─────────────────────┘ └┘ └┘
src └──┘└─────┘└┘└─────────────────────┘┴ ┴ └─
typ └──┘└─────┘└┘└─────────────────────┘┴└┘┴└┘└─
doc └──┘ └┘ ┴ ┴ └─
txt └──┘ └┘ ┴ ┴ └─
par └──┘ └┘ ┴ ┴ └─
pid └┘ └┘ ┴ ┴ ┴└
st └──────────┘└─────────────────────────────┘┴└
514
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
515 theorem sqrt_mul_self_eq_abs (x : ℝ) : sqrt (x * x) = abs x :=
id ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴
src ┴ └──┘ ┴ ┴ └─┘
typ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴
516 (le_total 0 x).elim
id └──────┘ ┴ └──┘
src └──────┘ └──┘
typ └──────┘ ┴ └──┘
517 (λ h, (sqrt_mul_self h).trans (abs_of_nonneg h).symm)
id ┴ └───────────┘ ┴ └───┘ └───────────┘ ┴ └──┘
src └───────────┘ └───┘ └───────────┘ └──┘
typ ┴ └───────────┘ ┴ └───┘ └───────────┘ ┴ └──┘
518 (λ h, by rw [← neg_mul_neg,
id ┴ └─────────┘
src └────┘└─────────┘└─
typ ┴ └────┘└─────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid └──┘ └─
st └────────────────┘└─
519 sqrt_mul_self (neg_nonneg.2 h), abs_of_nonpos h])
id └───────────┘ └────────┘ ┴ └───────────┘ ┴
src ───┘└───────────┘┴ └────────┘└─┘ └─┘└───────────┘┴ ┴
typ ───┘└───────────┘┴ └────────┘└─┘┴└─┘└───────────┘┴┴┴
doc ───┘ ┴ └─┘ └─┘ ┴ ┴
txt ───┘ ┴ └─┘ └─┘ ┴ ┴
par ───┘ ┴ └─┘ └─┘ ┴ ┴
pid ───┘ ┴ └─┘ └─┘ ┴ ┴
st ─────────────────────────────────┘└───────────────┘┴
520
521 theorem sqrt_sqr_eq_abs (x : ℝ) : sqrt (x ^ 2) = abs x :=
id ┴ └──┘ ┴ ┴ ┴ └─┘ ┴
src ┴ └──┘ ┴ ┴ └─┘
typ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴
522 by rw [pow_two, sqrt_mul_self_eq_abs]
id └─────┘ └──────────────────┘
src └──┘└─────┘└┘└──────────────────┘└─
typ └──┘└─────┘└┘└──────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────┘└────────────────────┘┴└
523
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
524 @[simp] theorem sqrt_zero : sqrt 0 = 0 :=
id └──┘ ┴
src └──┘ ┴
typ └──┘ ┴
doc └──┘
525 by simpa using sqrt_mul_self (le_refl _)
id └───────────┘ └─────┘
src └──────────┘└───────────┘┴ └─────┘└───
typ └──────────┘└───────────┘┴ └─────┘└───
doc └──────────┘ ┴ └───
txt └──────────┘ ┴ └───
par └──────────┘ ┴ └───
pid ┴└────┘ ┴ └─┘└
st └──────────────────────────────────────
526
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
527 @[simp] theorem sqrt_one : sqrt 1 = 1 :=
id └──┘ ┴
src └──┘ ┴
typ └──┘ ┴
doc └──┘
528 by simpa using sqrt_mul_self zero_le_one
id └───────────┘ └─────────┘
src └──────────┘└───────────┘┴└─────────┘└
typ └──────────┘└───────────┘┴└─────────┘└
doc └──────────┘ ┴ └
txt └──────────┘ ┴ └
par └──────────┘ ┴ └
pid ┴└────┘ ┴ └
st └──────────────────────────────────────
529
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
530 @[simp] theorem sqrt_le (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x ≤ sqrt y ↔ x ≤ y :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ └──┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
531 by rw [mul_self_le_mul_self_iff (sqrt_nonneg _) (sqrt_nonneg _),
id └──────────────────────┘ └─────────┘
src └──┘└──────────────────────┘┴ └──┘ └─────────┘└────
typ └──┘└──────────────────────┘┴ └──┘ └─────────┘└────
doc └──┘ ┴ └──┘ └────
txt └──┘ ┴ └──┘ └────
par └──┘ ┴ └──┘ └────
pid └┘ ┴ └──┘ └────
st └───────────────────────────────────────────────────────────┘└─
532 mul_self_sqrt hx, mul_self_sqrt hy]
id └───────────┘ └┘ └───────────┘ └┘
src ──────┘└───────────┘┴ └┘└───────────┘┴ └─
typ ──────┘└───────────┘┴└┘└┘└───────────┘┴└┘└─
doc ──────┘ ┴ └┘ ┴ └─
txt ──────┘ ┴ └┘ ┴ └─
par ──────┘ ┴ └┘ ┴ └─
pid ──────┘ ┴ └┘ ┴ ┴└
st ──────────────────────┘└────────────────┘┴└
533
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
534 @[simp] theorem sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x < sqrt y ↔ x < y :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ └──┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
535 lt_iff_lt_of_le_iff_le (sqrt_le hy hx)
id └────────────────────┘ └─────┘ └┘ └┘
src └────────────────────┘ └─────┘
typ └────────────────────┘ └─────┘ └┘ └┘
536
537 lemma sqrt_le_sqrt (h : x ≤ y) : sqrt x ≤ sqrt y :=
id ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
538 begin
st └─────
539 rw [mul_self_le_mul_self_iff (sqrt_nonneg _) (sqrt_nonneg _), (sqrt_prop _).2, (sqrt_prop _).2],
id └──────────────────────┘ └─────────┘ └───────┘ └───────┘
src └──┘└──────────────────────┘┴ └──┘ └─────────┘└───┘ └───────┘└─────┘ └───────┘└────┘
typ └──┘└──────────────────────┘┴ └──┘ └─────────┘└───┘ └───────┘└─────┘ └───────┘└────┘
doc └──┘ ┴ └──┘ └───┘ └─────┘ └────┘
txt └──┘ ┴ └──┘ └───┘ └─────┘ └────┘
par └──┘ ┴ └──┘ └───┘ └─────┘ └────┘
pid └┘ ┴ └──┘ └───┘ └─────┘ └────┘
st ─────────────────────────────────────────────────────────────┘└─────────────┘└───────────────┘└────
540 exact max_le_max (le_refl _) h
id └────────┘ └─────┘ ┴
src └────┘└────────┘┴ └─────┘└──┘ ┴
typ └────┘└────────┘┴ └─────┘└──┘┴┴
doc └────┘ ┴ └──┘ ┴
txt └────┘ ┴ └──┘ ┴
par └────┘ ┴ └──┘ ┴
pid ┴ ┴ └──┘ ┴
st ────────────────────────────────┘
541 end
st └─┘
542
543 lemma sqrt_le_left (hy : 0 ≤ y) : sqrt x ≤ y ↔ x ≤ y ^ 2 :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
544 begin
st └─────
545 rw [mul_self_le_mul_self_iff (sqrt_nonneg _) hy, pow_two],
id └──────────────────────┘ └─────────┘ └┘ └─────┘
src └──┘└──────────────────────┘┴ └─────────┘└──┘ └┘└─────┘┴
typ └──┘└──────────────────────┘┴ └─────────┘└──┘└┘└┘└─────┘┴
doc └──┘ ┴ └──┘ └┘ ┴
txt └──┘ ┴ └──┘ └┘ ┴
par └──┘ ┴ └──┘ └┘ ┴
pid └┘ ┴ └──┘ └┘ ┴
st ────────────────────────────────────────────────┘└───────┘└──
546 cases le_total 0 x with hx hx,
id └──────┘ ┴
src └────┘└──────┘└─┘ └─────────┘
typ └────┘└──────┘└─┘┴└─────────┘
doc └────┘ └─┘ └─────────┘
txt └────┘ └─┘ └─────────┘
par └────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ──────────────────────────────┘└─
547 { rw [mul_self_sqrt hx] },
id └───────────┘ └┘
src └──┘└───────────┘┴ └┘
typ └──┘└───────────┘┴└┘└┘
doc └──┘ ┴ └┘
txt └──┘ ┴ └┘
par └──┘ ┴ └┘
pid └┘ ┴ ┴┴
st ───┘└──────────────────┘┴┴└┘└
548 { have h1 : 0 ≤ y * y := mul_nonneg hy hy,
id ┴ ┴ ┴ └────────┘ └┘
src └──────────┘┴┴ ┴┴┴ └──┘└────────┘┴ ┴
typ └──────────┘┴┴ ┴┴┴┴└──┘└────────┘┴ ┴└┘
doc └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
par └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
pid └─────┘└───┘ ┴ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────┘└─
549 have h2 : x ≤ y * y := le_trans hx h1,
id ┴ ┴ └──────┘ └┘ └┘
src └────────┘ ┴ ┴ ┴ ┴ └──┘└──────┘┴ ┴
typ └────────┘┴┴ ┴ ┴ ┴┴└──┘└──────┘┴└┘┴└┘
doc └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
st ────────────────────────────────────────┘└─
550 simp [sqrt_eq_zero_of_nonpos, hx, h1, h2] }
id └────────────────────┘ └┘ └┘ └┘
src └────┘└────────────────────┘└┘ └┘ └┘ └┘
typ └────┘└────────────────────┘└┘└┘└┘└┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────┘└─
551 end
st ──┘
552
553 /- note: if you want to conclude `x ≤ sqrt y`, then use `le_sqrt_of_sqr_le`.
554 if you have `x > 0`, consider using `le_sqrt'` -/
555 lemma le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └──┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
556 by rw [mul_self_le_mul_self_iff hx (sqrt_nonneg _), pow_two, mul_self_sqrt hy]
id └──────────────────────┘ └┘ └─────────┘ └─────┘ └───────────┘ └┘
src └──┘└──────────────────────┘┴ ┴ └─────────┘└───┘└─────┘└┘└───────────┘┴ └─
typ └──┘└──────────────────────┘┴└┘┴ └─────────┘└───┘└─────┘└┘└───────────┘┴└┘└─
doc └──┘ ┴ ┴ └───┘ └┘ ┴ └─
txt └──┘ ┴ ┴ └───┘ └┘ ┴ └─
par └──┘ ┴ ┴ └───┘ └┘ ┴ └─
pid └┘ ┴ ┴ └───┘ └┘ ┴ ┴└
st └──────────────────────────────────────────────┘└───────┘└────────────────┘┴└
557
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
558 lemma le_sqrt' (hx : 0 < x) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
559 begin
st └─────
560 rw [mul_self_le_mul_self_iff (le_of_lt hx) (sqrt_nonneg _), pow_two],
id └──────────────────────┘ └──────┘ └┘ └─────────┘ └─────┘
src └──┘└──────────────────────┘┴ └──────┘┴ └┘ └─────────┘└───┘└─────┘┴
typ └──┘└──────────────────────┘┴ └──────┘┴└┘└┘ └─────────┘└───┘└─────┘┴
doc └──┘ ┴ ┴ └┘ └───┘ ┴
txt └──┘ ┴ ┴ └┘ └───┘ ┴
par └──┘ ┴ ┴ └┘ └───┘ ┴
pid └┘ ┴ ┴ └┘ └───┘ ┴
st ───────────────────────────────────────────────────────────┘└───────┘└──
561 cases le_total 0 y with hy hy,
id └──────┘ ┴
src └────┘└──────┘└─┘ └─────────┘
typ └────┘└──────┘└─┘┴└─────────┘
doc └────┘ └─┘ └─────────┘
txt └────┘ └─┘ └─────────┘
par └────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ──────────────────────────────┘└─
562 { rw [mul_self_sqrt hy] },
id └───────────┘ └┘
src └──┘└───────────┘┴ └┘
typ └──┘└───────────┘┴└┘└┘
doc └──┘ ┴ └┘
txt └──┘ ┴ └┘
par └──┘ ┴ └┘
pid └┘ ┴ ┴┴
st ───┘└──────────────────┘┴┴└┘└
563 { have h1 : 0 < x * x := mul_pos hx hx,
id ┴ ┴ ┴ └─────┘ └┘
src └──────────┘┴┴ ┴┴┴ └──┘└─────┘┴ ┴
typ └──────────┘┴┴ ┴┴┴┴└──┘└─────┘┴ ┴└┘
doc └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
par └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
pid └─────┘└───┘ ┴ ┴ ┴ └──┘ ┴ ┴
st ───────────────────────────────────────┘└─
564 have h2 : ¬x * x ≤ y := not_le_of_lt (lt_of_le_of_lt hy h1),
id ┴ ┴ ┴ ┴ └──────────┘ └────────────┘ └┘ └┘
src └────────┘┴ ┴ ┴ ┴┴┴ └──┘└──────────┘┴ └────────────┘┴ ┴ ┴
typ └────────┘┴ ┴ ┴┴┴┴┴┴└──┘└──────────┘┴ └────────────┘┴└┘┴└┘┴
doc └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
565 simp [sqrt_eq_zero_of_nonpos, hy, h1, h2] }
id └────────────────────┘ └┘ └┘ └┘
src └────┘└────────────────────┘└┘ └┘ └┘ └┘
typ └────┘└────────────────────┘└┘└┘└┘└┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────┘└─
566 end
st ──┘
567
568 lemma le_sqrt_of_sqr_le (h : x ^ 2 ≤ y) : x ≤ sqrt y :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
569 begin
st └─────
570 cases lt_or_ge 0 x with hx hx,
id └──────┘ ┴
src └────┘└──────┘└─┘ └─────────┘
typ └────┘└──────┘└─┘┴└─────────┘
doc └────┘ └─┘ └─────────┘
txt └────┘ └─┘ └─────────┘
par └────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ──────────────────────────────┘└─
571 { rwa [le_sqrt' hx] },
id └──────┘ └┘
src └───┘└──────┘┴ └┘
typ └───┘└──────┘┴└┘└┘
doc └───┘ ┴ └┘
txt └───┘ ┴ └┘
par └───┘ ┴ └┘
pid └┘ ┴ ┴┴
st ───┘└──────────────┘┴┴└┘└
572 { exact le_trans hx (sqrt_nonneg y) }
id └──────┘ └┘ └─────────┘ ┴
src └────┘└──────┘┴ ┴ └─────────┘┴ └┘
typ └────┘└──────┘┴└┘┴ └─────────┘┴┴└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ─────────────────────────────────────┘└─
573 end
st ──┘
574
575 @[simp] theorem sqrt_inj (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x = sqrt y ↔ x = y :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ └──┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
576 by simp [le_antisymm_iff, hx, hy]
id └─────────────┘ └┘ └┘
src └────┘└─────────────┘└┘ └┘ └─
typ └────┘└─────────────┘└┘└┘└┘└┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └───────────────────────────────
577
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
578 @[simp] theorem sqrt_eq_zero (h : 0 ≤ x) : sqrt x = 0 ↔ x = 0 :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
579 by simpa using sqrt_inj h (le_refl _)
id └──────┘ ┴ └─────┘
src └──────────┘└──────┘┴ ┴ └─────┘└───
typ └──────────┘└──────┘┴┴┴ └─────┘└───
doc └──────────┘ ┴ ┴ └───
txt └──────────┘ ┴ ┴ └───
par └──────────┘ ┴ ┴ └───
pid ┴└────┘ ┴ ┴ └─┘└
st └───────────────────────────────────
580
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
581 theorem sqrt_eq_zero' : sqrt x = 0 ↔ x ≤ 0 :=
id └──┘ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴
582 (le_total x 0).elim
id └──────┘ ┴ └──┘
src └──────┘ └──┘
typ └──────┘ ┴ └──┘
583 (λ h, by simp [h, sqrt_eq_zero_of_nonpos])
id ┴ ┴ └────────────────────┘
src └────┘ └┘└────────────────────┘┴
typ ┴ └────┘┴└┘└────────────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └───────────────────────────────┘
584 (λ h, by simp [h]; simp [le_antisymm_iff, h])
id ┴ ┴ └─────────────┘ ┴
src └────┘ ┴ └────┘└─────────────┘└┘ ┴
typ ┴ └────┘┴┴ └────┘└─────────────┘└┘┴┴
doc └────┘ ┴ └────┘ └┘ ┴
txt └────┘ ┴ └────┘ └┘ ┴
par └────┘ ┴ └────┘ └┘ ┴
pid ┴┴ ┴ ┴┴ └┘ ┴
st └──────────────────────────────────┘
585
586 @[simp] theorem sqrt_pos : 0 < sqrt x ↔ 0 < x :=
id ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
587 lt_iff_lt_of_le_iff_le (iff.trans
id └────────────────────┘ └───────┘
src └────────────────────┘ └───────┘
typ └────────────────────┘ └───────┘
588 (by simp [le_antisymm_iff, sqrt_nonneg]) sqrt_eq_zero')
id └─────────────┘ └─────────┘ └───────────┘
src └────┘└─────────────┘└┘└─────────┘┴ └───────────┘
typ └────┘└─────────────┘└┘└─────────┘┴ └───────────┘
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └──────────────────────────────────┘
589
590 @[simp] theorem sqrt_mul' (x) {y : ℝ} (hy : 0 ≤ y) : sqrt (x * y) = sqrt x * sqrt y :=
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘
591 begin
st └─────
592 cases le_total 0 x with hx hx,
id └──────┘ ┴
src └────┘└──────┘└─┘ └─────────┘
typ └────┘└──────┘└─┘┴└─────────┘
doc └────┘ └─┘ └─────────┘
txt └────┘ └─┘ └─────────┘
par └────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ──────────────────────────────┘└─
593 { refine (mul_self_inj_of_nonneg _ (mul_nonneg _ _)).1 _; try {apply sqrt_nonneg},
id └────────────────────┘ └────────┘ └─────────┘
src └─────┘ └────────────────────┘└─┘ └────────┘└────────┘ └───┘└────┘└─────────┘┴
typ └─────┘ └────────────────────┘└─┘ └────────┘└────────┘ └───┘└────┘└─────────┘┴
doc └─────┘ └─┘ └────────┘ └───┘└────┘ ┴
txt └─────┘ └─┘ └────────┘ └───┘└────┘ ┴
par └─────┘ └─┘ └────────┘ └───┘└────┘ ┴
pid ┴ └─┘ └────────┘ └──────┘ ┴
st ───┘└───────────────────────────────────────────────────────────┘└───────────────┘└┘└
594 rw [mul_self_sqrt (mul_nonneg hx hy), mul_assoc,
id └───────────┘ └────────┘ └┘ └┘ └───────┘
src └──┘└───────────┘┴ └────────┘┴ ┴ └─┘└───────┘└─
typ └──┘└───────────┘┴ └────────┘┴└┘┴└┘└─┘└───────┘└─
doc └──┘ ┴ ┴ ┴ └─┘ └─
txt └──┘ ┴ ┴ ┴ └─┘ └─
par └──┘ ┴ ┴ ┴ └─┘ └─
pid └┘ ┴ ┴ ┴ └─┘ └─
st ───────────────────────────────────────┘└─────────┘└─
595 mul_left_comm (sqrt y), mul_self_sqrt hy, ← mul_assoc, mul_self_sqrt hx] },
id └───────────┘ └──┘ ┴ └───────────┘ └┘ └───────┘ └───────────┘ └┘
src ───────┘└───────────┘┴ └──┘┴ └─┘└───────────┘┴ └──┘└───────┘└┘└───────────┘┴ └┘
typ ───────┘└───────────┘┴ └──┘┴┴└─┘└───────────┘┴└┘└──┘└───────┘└┘└───────────┘┴└┘└┘
doc ───────┘ ┴ ┴ └─┘ ┴ └──┘ └┘ ┴ └┘
txt ───────┘ ┴ ┴ └─┘ ┴ └──┘ └┘ ┴ └┘
par ───────┘ ┴ ┴ └─┘ ┴ └──┘ └┘ ┴ └┘
pid ───────┘ ┴ ┴ └─┘ ┴ └──┘ └┘ ┴ ┴┴
st ─────────────────────────────┘└────────────────┘└───────────┘└────────────────┘┴┴└┘└
596 { rw [sqrt_eq_zero'.2 (mul_nonpos_of_nonpos_of_nonneg hx hy),
id └───────────┘ └────────────────────────────┘ └┘ └┘
src └──┘└───────────┘└─┘ └────────────────────────────┘┴ ┴ └──
typ └──┘└───────────┘└─┘ └────────────────────────────┘┴└┘┴└┘└──
doc └──┘ └─┘ ┴ ┴ └──
txt └──┘ └─┘ ┴ ┴ └──
par └──┘ └─┘ ┴ ┴ └──
pid └┘ └─┘ ┴ ┴ └──
st ─────────────────────────────────────────────────────────────┘└─
597 sqrt_eq_zero'.2 hx, zero_mul] }
id └───────────┘ └┘ └──────┘
src ───────┘└───────────┘└─┘ └┘└──────┘└┘
typ ───────┘└───────────┘└─┘└┘└┘└──────┘└┘
doc ───────┘ └─┘ └┘ └┘
txt ───────┘ └─┘ └┘ └┘
par ───────┘ └─┘ └┘ └┘
pid ───────┘ └─┘ └┘ ┴┴
st ─────────────────────────┘└────────┘┴┴└─
598 end
st ──┘
599
600 @[simp] theorem sqrt_mul (hx : 0 ≤ x) (y : ℝ) : sqrt (x * y) = sqrt x * sqrt y :=
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘
601 by rw [mul_comm, sqrt_mul' _ hx, mul_comm]
id └──────┘ └───────┘ └┘ └──────┘
src └──┘└──────┘└┘└───────┘└─┘ └┘└──────┘└─
typ └──┘└──────┘└┘└───────┘└─┘└┘└┘└──────┘└─
doc └──┘ └┘ └─┘ └┘ └─
txt └──┘ └┘ └─┘ └┘ └─
par └──┘ └┘ └─┘ └┘ └─
pid └┘ └┘ └─┘ └┘ ┴└
st └───────────┘└──────────────┘└────────┘┴└
602
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
603 @[simp] theorem sqrt_inv (x : ℝ) : sqrt x⁻¹ = (sqrt x)⁻¹ :=
id ┴ └──┘ ┴└┘ ┴ └──┘ ┴ └┘
src ┴ └──┘ └┘ ┴ └──┘ └┘
typ ┴ └──┘ ┴└┘ ┴ └──┘ ┴ └┘
doc └──┘
604 (le_or_lt x 0).elim
id └──────┘ ┴ └──┘
src └──────┘ └──┘
typ └──────┘ ┴ └──┘
605 (λ h, by simp [sqrt_eq_zero'.2, inv_nonpos, h])
id ┴ └───────────┘ └────────┘ ┴
src └────┘└───────────┘└──┘└────────┘└┘ ┴
typ ┴ └────┘└───────────┘└──┘└────────┘└┘┴┴
doc └────┘ └──┘ └┘ ┴
txt └────┘ └──┘ └┘ ┴
par └────┘ └──┘ └┘ ┴
pid ┴┴ └──┘ └┘ ┴
st └────────────────────────────────────┘
606 (λ h, by rw [
id ┴
src └────
typ ┴ └────
doc └────
txt └────
par └────
pid └──
st └─────
607 ← mul_self_inj_of_nonneg (sqrt_nonneg _) (le_of_lt $ inv_pos $ sqrt_pos.2 h),
id └────────────────────┘ └─────────┘ └──────┘ └─────┘ └──────┘ ┴
src ─────┘└────────────────────┘┴ └─────────┘└──┘ └──────┘┴ ┴└─────┘┴ ┴└──────┘└─┘ └──
typ ─────┘└────────────────────┘┴ └─────────┘└──┘ └──────┘┴ ┴└─────┘┴ ┴└──────┘└─┘┴└──
doc ─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └──
txt ─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └──
par ─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └──
pid ─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └──
st ───────────────────────────────────────────────────────────────────────────────┘└─
608 mul_self_sqrt (le_of_lt $ inv_pos h), ← mul_inv', mul_self_sqrt (le_of_lt h)])
id └───────────┘ └──────┘ └─────┘ ┴ └──────┘ └───────────┘ └──────┘ ┴
src ───┘└───────────┘┴ └──────┘┴ ┴└─────┘┴ └───┘└──────┘└┘└───────────┘┴ └──────┘┴ └┘
typ ───┘└───────────┘┴ └──────┘┴ ┴└─────┘┴┴└───┘└──────┘└┘└───────────┘┴ └──────┘┴┴└┘
doc ───┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ └┘
txt ───┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ └┘
par ───┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ └┘
pid ───┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ └┘
st ───────────────────────────────────────┘└──────────┘└──────────────────────────┘┴
609
610 @[simp] theorem sqrt_div (hx : 0 ≤ x) (y : ℝ) : sqrt (x / y) = sqrt x / sqrt y :=
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘
611 by rw [division_def, sqrt_mul hx, sqrt_inv]; refl
id └──────────┘ └──────┘ └┘ └──────┘
src └──┘└──────────┘└┘└──────┘┴ └┘└──────┘┴ └────
typ └──┘└──────────┘└┘└──────┘┴└┘└┘└──────┘┴ └────
doc └──┘ └┘ ┴ └┘ ┴ └────
txt └──┘ └┘ ┴ └┘ ┴ └────
par └──┘ └┘ ┴ └┘ ┴ └────
pid └┘ └┘ ┴ └┘ ┴ └
st └───────────────┘└───────────┘└────────┘┴└──────
612
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
613 attribute [irreducible] real.le
id └─────┘
src └─────┘
typ └─────┘
doc └─────────┘
614
615 end real